Abstract—Real-time systems demand functional as well as temporal correctness. Complex interactions with the environment and strict adherence to time bounds are main characteristics of these systems. The use of formal methods is a natural choice for real-time system development. Formal models are more rigorous in nature and ensure completeness. If a system is highly sensitive to time delays, time behaviour of real-time system must be specified through formal languages. Petri nets, state charts and UML can be used to represent time behaviour, but these techniques are lesser effective than formal languages. The strength of formal languages depends upon completeness and possibility of partial mathematical verification. In order to study time behaviour, we have surveyed existing formal languages used to model real-time systems. We have selected typical languages that are supposed to represent entire set of real-time formal languages. Some parameters are defined to critically evaluate these languages. We have analysed and compared formal languages for real-time systems using our defined evaluation criteria. As a result of our analysis, we conclude that all languages incorporate special constructs to capture time behaviour. Effectiveness of these constructs can be compared on the basis of the capability of the languages to specify time domain. We also conclude that there is an ardent need to standardise formal languages used to specify real-time systems.
Index Terms—Formal languages, real-time systems, temporal logic, first order logic, mathematical verification, time domains, semantics and ontology.
The authors are with Center for Software Dependability, Muhammad Ali Jinnah University (MAJU), Islamabad, Pakistan (e-mail: email@example.com, firstname.lastname@example.org).
Cite: Aftab Ali Haider and Aamer Nadeem, "Formal Modelling Languages to Specify Real-Time Systems: A Survey," International Journal of Future Computer and Communication vol. 2, no. 2 pp. 130-133, 2013.