Issue No. 03 - March (1998 vol. 24)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.667880
<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.