[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php
Bibliographic Item (1.0)
- Angelo Gargantini & angelo Morzenti
Automated Deductive Requirements analysis of Critical systems
- ACM TOSEM Trans Software Engineering & Methodology V10n3(Jul 2001)pp255-307
- =DEMO FORMAL REQUIREMENTS ANALYSIS SRA LOGIC
TD TOOL PVS Non-Zeno
- TD:="Time dependent".
- TRIO -- see Federer
- DUC::="Device under Construction".
- events (point based predicates) : true at a single time and not immediately before or after.
- interval-Based predicates: if true then true in some before or after interval nearby and if false then false nearby..
- left and right closed interval-based predicates and variables. Left continuous interval based (lci) means that predicate has the same value at a given time as it had in a previous neighboring interval.
- non-Zeno predicates and variable. Named after Zeno's paradoxes. finite variability. physical meaningful. One can talk about the value immediately before or after the current time.
- non_Zeno(A)::=(UpToNow(not A) or UpToNow(A)) and (NowOn(not A) NowOn(A) ),
- UpToNow(A)::= t+>for some d1>0, all d2:(0..d1) ( A (t-d2)),
- NowOn(A)::= t+>for some d1>0, all d2:(0..d1) ( A (t+d2))
Search for bibliographic items containing a matching string.
Search for a specific bibliographic item by name.
To see the complete bibliography (1Mb+) select:[Bibliography]