Specification and Validation of a Real-Time Parallel Kernel using LOTOS

Cléver Guareis de farias, Luis Ferreira Pires, Wanderley Lopes de Souza, Célio Estevan Moron

    Research output: Book/Report › Report › Other research output

    2 Citations (Scopus)
    5 Downloads (Pure)

    Abstract

    This paper presents and discusses the LOTOS specification of a real-time parallel kernel. The purpose of this specification exercise has been to evaluate LOTOS with respect to its capabilities to model real-time features with a realistic industrial product. LOTOS was used to produce the formal specification of TRANS-RTXC, which is a real-time parallel kernel developed by Intelligent Systems international. This paper shows that although timing constraints cannot be explicitly represented in LOTOS, the language is suitable for the specification of co-ordination of real-time tasks, which is the main functionality of the real-time kernel. This paper also discusses the validation process of the kernel specification and the role of tools in this validation process. We believe that our experience (use of structuring techniques, use of validation methods and tools, etc) is valuable for designers who want to apply formal models in their design or analysis tasks.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Publication statusPublished - Jul 2001

    Publication series

    NameCTIT technical report series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.TR-CTIT-01-30
    ISSN (Print)1381-3625

    Keywords

    • SCS-Services

    Access to Document

    • ReportFinal published version, 107 KB

      Fingerprint

      Dive into the research topics of 'Specification and Validation of a Real-Time Parallel Kernel using LOTOS'. Together they form a unique fingerprint.
      View full fingerprint
      • 2 Citations
      • 1 Conference contribution

      • Specification and Validation of a Real-Time Parallel Kernel using LOTOS

        de farias, C. R. G., Pires, L. F., de Souza, W. & Moron, C. E., 15 Aug 2001, MASCOTS 2001: Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. Das, S. R., Nicol, D. & Perrone, F. (eds.). Piscataway, NJ: University of Cincinatti, p. 7-14 8 p. (MASCOTS, Proceedings International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems; vol. 2001, no. 9).

        Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

        Open Access
        File
        163 Downloads (Pure)

      Cite this