On-the-fly model checking from interval logic specifications

Future Interval Logic (FIL) and its intuitive graphical representation, Graphical Interval Logic (GIL), can be used as the formal description language of model checking tools to verify hardware and software systems. An interval clearly defines the temporal scope over which properties are evaluated. From interval formulas specifying the temporal behavior of a system we obtain their semantically equivalent B

• Type: Journal
• Year: 2002
• Where: SIGPLAN
• Authors: Miguel J. Hornos, Manuel I. Capel
• Keywords: Future Interval Logic, Graphical Interval Logic, Interval Logic, SIGPLAN 2002, System Software