[CSUSB]>> [CNS]>> [CSE]>> [R J Botting]>> biba.php

Bibliographic Item (1.0)

GargantiniMorzenti01

  1. Angelo Gargantini & angelo Morzenti Automated Deductive Requirements analysis of Critical systems
  2. ACM TOSEM Trans Software Engineering & Methodology V10n3(Jul 2001)pp255-307
  3. =DEMO FORMAL REQUIREMENTS ANALYSIS SRA LOGIC [TRIO] TD TOOL PVS Non-Zeno
  4. TD:="Time dependent".
  5. TRIO -- see Federer
  6. DUC::="Device under Construction".
  7. events (point based predicates) : true at a single time and not immediately before or after.
  8. interval-Based predicates: if true then true in some before or after interval nearby and if false then false nearby..
  9. 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.
  10. 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.
  11. non_Zeno(A)::=(UpToNow(not A) or UpToNow(A)) and (NowOn(not A) NowOn(A) ),
  12. UpToNow(A)::= t+>for some d1>0, all d2:(0..d1) ( A (t-d2)),
  13. NowOn(A)::= t+>for some d1>0, all d2:(0..d1) ( A (t+d2))

Search for bibliographic items containing a matching string.


(Search uses POSIX regular expressions and ignores case)

Search for a specific bibliographic item by name.



To see the complete bibliography (1Mb+) select:[Bibliography]