Specification, validation, and verification of time-critical systems

Shiuhpyng Shieh*, Jun Nan Chen

*Corresponding author for this work

Research output: Contribution to journalArticle

Abstract

In this paper, we propose a new formalism, named the Timed Communicating Finite State Machine (Timed CFSM), for specifying and verifying time-critical systems. Timed CFSM preserves the advantages of CFSM, such as the ability to express communication, synchronization and concurrency in computer systems. A given time-dependent specification can be formalized as a Timed CFSM, from which the reachability graph is constructed to verify the correctness of the specification. To cope with the space explosion problem from which all reachability analysis methods suffer, we propose a space reduction algorithm to meet the space constraint of the verification environment.

Original languageEnglish
Pages (from-to)460-469
Number of pages10
JournalComputer Communications
Volume21
Issue number5
DOIs
StatePublished - 1 May 1998

Keywords

  • Path approach
  • Reachability analysis
  • Specification
  • The space explosion problem
  • Time-critical systems
  • Validation
  • Verification

Fingerprint Dive into the research topics of 'Specification, validation, and verification of time-critical systems'. Together they form a unique fingerprint.

  • Cite this