Formal specification and verification of embedded system with shared resources

Ki Seok Bang, Jin Young Choi, Sung Ho Jang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In order to achieve a correct implementation, it has been known that a specification and its verification in early design stage are important, especially during developing safety critical or embedded real-time systems. Statechart is a widely used graphical formal specification language; however, it is not trivial to specify software systems in case that shared resources have to be specified due to no concept of shared resources. In this paper, we present an extension of Statechart, Statechart with Shared Resources, the semantics of which are based on a process algebra, and we demonstrate its expressiveness by specifying μC/OS II, one of the well-known real-time commercial operating systems used in various fields. Using a resource concept in Statechart, it is clear for designer to capture design requirements efficiently and can verify the requirement specifications formally using a tool called VERSA.

Original languageEnglish
Title of host publicationProceedings of the International Workshop on Rapid System Prototyping
Pages8-14
Number of pages7
Publication statusPublished - 2004
EventProceedings - 15th IEEE International Workshop on Rapid Systems Prototyping - Geneva, Switzerland
Duration: 2004 Jun 282004 Jun 30

Other

OtherProceedings - 15th IEEE International Workshop on Rapid Systems Prototyping
CountrySwitzerland
CityGeneva
Period04/6/2804/6/30

    Fingerprint

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Cite this

Bang, K. S., Choi, J. Y., & Jang, S. H. (2004). Formal specification and verification of embedded system with shared resources. In Proceedings of the International Workshop on Rapid System Prototyping (pp. 8-14)