• Jan 04, 2024 News!IJFCC will adopt Article-by-Article Work Flow
  • Mar 30, 2026 News!Vol.15, No.1 has been published with online version.   [Click]
  • Oct 24, 2025 News!Special Announcement: Temporary APC Waiver   [Click]
General Information
    • ISSN: 2010-3751 (Print)
    • Frequency: Semi-annual
    • DOI: 10.18178/IJFCC
    • Editor-in-Chief: Prof. Pascal Lorenz
    • Executive Editor: Ms. Tina Yuen
    • Abstracting/ Indexing: Crossref, Electronic Journals LibraryGoogle Scholar, EBSCO, etc.
    • E-mail:  editor@ijfcc.org
    • Article Processing Charge: 500 USD
Editor-in-chief

Prof. Pascal Lorenz
University of Haute Alsace, France
 
It is my honor to be the Editor-in-Chief of IJFCC. The journal publishes good papers in the field of future computer and communication. Hopefully, IJFCC will become a recognized journal among the readers in the filed of future computer and communication.

IJFCC 2013 Vol.2(2): 130-133 ISSN: 2010-3751
DOI: 10.7763/IJFCC.2013.V2.136

Formal Modelling Languages to Specify Real-Time Systems: A Survey

Aftab Ali Haider and Aamer Nadeem

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: aftab775@yahoo.com, anadeem@jinnah.edu.pk).

[PDF]

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.

Copyright © 2012-2026. International Journal of Future Computer and Communication. Unless otherwise stated.

E-mail: editor@ijfcc.org