Skip to main navigation Skip to search Skip to main content

A method on specification and verification of component interaction in real-time reactive systems

  • Yangli Jia*
  • , Zhoujun Li
  • , Zhenling Zhang
  • , Shengxian Xie
  • *Corresponding author for this work
  • Beihang University
  • Liaocheng University

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

We present Timed Component-Interaction Automata with Cost (TCIAC) to specify and verify component interaction behavior, timing cost and timing constraint information in component-based real-time reactive systems. TCIAC extends the description ability of component interaction automata by binding each action with a time interval and a timing cost value. The timing cost values of sequence and parallel actions can be worked out using a timing cost computing semiring we presented in this paper. TCIAC models of real-time components can be composed together based on the TCIAC composition definition. We discuss the application of TCIAC through a simple railroad crossing control system. We model the system using TCIAC for specifying and verifying the timeliness and other trustworthiness properties of component interaction.

Original languageEnglish
Title of host publicationProceedings - 2008 International Conference on Advanced Computer Theory and Engineering, ICACTE 2008
Pages388-392
Number of pages5
DOIs
StatePublished - 2008
Event2008 International Conference on Advanced Computer Theory and Engineering, ICACTE 2008 - Phuket, Thailand
Duration: 20 Dec 200822 Dec 2008

Publication series

NameProceedings - 2008 International Conference on Advanced Computer Theory and Engineering, ICACTE 2008

Conference

Conference2008 International Conference on Advanced Computer Theory and Engineering, ICACTE 2008
Country/TerritoryThailand
CityPhuket
Period20/12/0822/12/08

Fingerprint

Dive into the research topics of 'A method on specification and verification of component interaction in real-time reactive systems'. Together they form a unique fingerprint.

Cite this