Extending statecharts with temporal logic
- 1 March 1998
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 24 (3) , 216-231
- https://doi.org/10.1109/32.667880
Abstract
The task of designing large real-time reactive systems, which interact continuously with their environment and exhibit concurrency properties, is a challenging one. In this paper, we explore the utility of a combination of behavior and function specification languages in specifying such systems and verifying their properties. An existing specification language, statecharts, is used to specify the behavior of real-time reactive systems, while a new logic-based language called FNLOG (based on first-order predicate calculus and temporal logic. is designed to express the system functions over real time. Two types of system properties, intrinsic and structural, are proposed. It is shown that both types of system properties are expressible in FNLOG and may be verified by logical deduction, and also hold for the corresponding behavior specificationKeywords
This publication has 42 references indexed in Scilit:
- A visual toolset for the design of real-time discrete-event systemsIEEE Transactions on Control Systems Technology, 1997
- Formal methods for the specification and design of real-time safety critical systemsJournal of Systems and Software, 1992
- Applications of temporal logic to the specification of real time systemsPublished by Springer Nature ,1988
- Specifying graceful degradation in distributed systemsPublished by Association for Computing Machinery (ACM) ,1987
- In Transition From Global to Modular Temporal Reasoning about ProgramsPublished by Springer Nature ,1985
- A rigorous approach to fault-tolerant system developmentPublished by Springer Nature ,1984
- Modular Verification of Computer Communication ProtocolsIEEE Transactions on Communications, 1983
- Formal Specification and Mechanical Verification of SIFT: A Fault-Tolerant Flight Control SystemIEEE Transactions on Computers, 1982
- Verifying Concurrent Processes Using Temporal LogicPublished by Springer Nature ,1982
- Principles of proving concurrent programs in GypsyPublished by Association for Computing Machinery (ACM) ,1979