The Community for Technology Leaders
Green Image
Issue No. 03 - March (1998 vol. 24)
ISSN: 0098-5589
pp: 216-231
<p><b>Abstract</b>—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, <it>statecharts</it>, is used to specify the behavior of real-time reactive systems, while a new logic-based language called <it>FNLOG</it> (based on first-order predicate calculus and temporal logic, is designed to express the system functions over real time. Two types of system properties, <it>intrinsic</it> and <it>structural</it>, 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 specification.</p>
Concurrency, FNLOG, formal specifications, reactive systems, real-time, robotics, statecharts, specification languages, state-machines, temporal logic.

A. Sowmya and S. Ramesh, "Extending Statecharts with Temporal Logic," in IEEE Transactions on Software Engineering, vol. 24, no. , pp. 216-231, 1998.
94 ms
(Ver 3.3 (11022016))