Multi-level specification and verification of real-time software
- 4 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The authors present a state-based approach for specification of real-time software at multiple levels of abstraction. In this approach, specification at each level is performed in terms of a hierarchical multistate (HMS) machine, with the higher levels defining requirements and the lower levels indicating methods of achieving the requirements. This approach leads to a considerable simplification of the specification process; it can lead to reusability of specifications and is fundamentally different from the refinement approach. A restricted method of verifying the consistency of multilevel specifications is also presented. By the use of this method, necessary scheduling of concurrent tasks to satisfy a complex set of logical and temporal constraints can often be derived Author(s) Gabrielian, Armen Thomson-CSF Inc., Palo Alto, CA, USA Franklin, M.K.Keywords
This publication has 7 references indexed in Scilit:
- A transformational method for verifying safety properties in real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Semantics of Modechart in real time logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- State-based specification of complex real-time systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- The existence of refinement mappingsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Statecharts: a visual formalism for complex systemsScience of Computer Programming, 1987
- Verifying SecurityACM Computing Surveys, 1981
- Proving the Correctness of Multiprocess ProgramsIEEE Transactions on Software Engineering, 1977