Formal specification and verification of embedded system with shared resources

Ki Seok Bang, Jin Young Choi, Sung Ho Jang

Research output: Contribution to journalConference articlepeer-review


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
Pages (from-to)8-14
Number of pages7
JournalProceedings of the International Workshop on Rapid System Prototyping
Publication statusPublished - 2004
EventProceedings - 15th IEEE International Workshop on Rapid Systems Prototyping - Geneva, Switzerland
Duration: 2004 Jun 282004 Jun 30

ASJC Scopus subject areas

  • General Computer Science


Dive into the research topics of 'Formal specification and verification of embedded system with shared resources'. Together they form a unique fingerprint.

Cite this