Timing properties analysis of real-time embedded systems with AADL model using model checking

Hanbo Wang, Xingshe Zhou, Yunwei Dong, Lei Tang

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

4 Scopus citations

Abstract

A novel approach to analyze timing properties of real-time embedded systems based on the model-driven architecture is proposed in this paper. The scheduling model which describes components of software and hardware as well as the interacting and binding relations of components is abstracted from an AADL model. The task deadline at the component lever and the end-to-end latency at the system lever are analyzed by specifying the scheduling model with the satisfiability modulo theories. An analysis tool is developed to work with the AADL developing environment to analyze the timing properties of the AADL model. The experiment results demonstrate the running performance of the proposed approach.

Original languageEnglish
Title of host publicationProceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010
Pages1019-1023
Number of pages5
DOIs
StatePublished - 2010
Event2010 1st IEEE International Conference on Progress in Informatics and Computing, PIC 2010 - Shanghai, China
Duration: 10 Dec 201012 Dec 2010

Publication series

NameProceedings of the 2010 IEEE International Conference on Progress in Informatics and Computing, PIC 2010
Volume2

Conference

Conference2010 1st IEEE International Conference on Progress in Informatics and Computing, PIC 2010
Country/TerritoryChina
CityShanghai
Period10/12/1012/12/10

Keywords

  • AADL
  • Model checking
  • Model-driven architecture
  • Timing properties

Fingerprint

Dive into the research topics of 'Timing properties analysis of real-time embedded systems with AADL model using model checking'. Together they form a unique fingerprint.

Cite this