Record Details

Extending statecharts with temporal logic

DSpace at IIT Bombay

View Archive Info
 
 
Field Value
 
Title Extending statecharts with temporal logic
 
Creator SOWMYA, A
RAMESH, S
 
Subject communication protocols
specification
verification
programs
systems
language
concurrency
fnlog
formal specifications
reactive systems
real-time
robotics
statecharts
specification languages
state-machines
temporal logic
 
Description 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 specification.
 
Publisher IEEE COMPUTER SOC
 
Date 2011-07-31T14:01:27Z
2011-12-26T12:53:02Z
2011-12-27T05:40:07Z
2011-07-31T14:01:27Z
2011-12-26T12:53:02Z
2011-12-27T05:40:07Z
1998
 
Type Article
 
Identifier IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 24(3), 216-231
0098-5589
http://dx.doi.org/10.1109/32.667880
http://dspace.library.iitb.ac.in/xmlui/handle/10054/8143
http://hdl.handle.net/10054/8143
 
Language en