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

    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
    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

    Fingerprint

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

    Cite this