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: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    30 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
    Title of host publication MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems
    EditorsS.R. Das, D. Nicol, F. Perrone
    PublisherUniversity of Cincinatti
    Pages7-14
    Number of pages8
    ISBN (Print)0-7695-1315-8
    DOIs
    Publication statusPublished - 15 Aug 2001
    Event9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS 2001 - Cincinatti, United States
    Duration: 15 Aug 200118 Aug 2001
    Conference number: 9

    Conference

    Conference9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS 2001
    Abbreviated titleMASCOTS
    CountryUnited States
    CityCincinatti
    Period15/08/0118/08/01

    Fingerprint

    Specification languages
    Specifications
    Intelligent systems

    Keywords

    • METIS-204031
    • IR-37117

    Cite this

    Guareis de farias, C., Ferreira Pires, L., Lopes de Souza, W., & Moron, C. E. (2001). Specification and Validation of a Real-Time Parallel Kernel using LOTOS. In S. R. Das, D. Nicol, & F. Perrone (Eds.), MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (pp. 7-14). University of Cincinatti. https://doi.org/10.1109/MASCOT.2001.948848
    Guareis de farias, Cléver ; Ferreira Pires, Luis ; Lopes de Souza, Wanderley ; Moron, Célio Estevan. / Specification and Validation of a Real-Time Parallel Kernel using LOTOS. MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. editor / S.R. Das ; D. Nicol ; F. Perrone. University of Cincinatti, 2001. pp. 7-14
    @inproceedings{27da68e77b4a4d00bfe61474767db4be,
    title = "Specification and Validation of a Real-Time Parallel Kernel using LOTOS",
    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",
    keywords = "METIS-204031, IR-37117",
    author = "{Guareis de farias}, Cl{\'e}ver and {Ferreira Pires}, Luis and {Lopes de Souza}, Wanderley and Moron, {C{\'e}lio Estevan}",
    year = "2001",
    month = "8",
    day = "15",
    doi = "10.1109/MASCOT.2001.948848",
    language = "English",
    isbn = "0-7695-1315-8",
    pages = "7--14",
    editor = "S.R. Das and D. Nicol and F. Perrone",
    booktitle = "MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems",
    publisher = "University of Cincinatti",

    }

    Guareis de farias, C, Ferreira Pires, L, Lopes de Souza, W & Moron, CE 2001, Specification and Validation of a Real-Time Parallel Kernel using LOTOS. in SR Das, D Nicol & F Perrone (eds), MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. University of Cincinatti, pp. 7-14, 9th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS 2001, Cincinatti, United States, 15/08/01. https://doi.org/10.1109/MASCOT.2001.948848

    Specification and Validation of a Real-Time Parallel Kernel using LOTOS. / Guareis de farias, Cléver; Ferreira Pires, Luis; Lopes de Souza, Wanderley; Moron, Célio Estevan.

    MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. ed. / S.R. Das; D. Nicol; F. Perrone. University of Cincinatti, 2001. p. 7-14.

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

    TY - GEN

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

    AU - Guareis de farias, Cléver

    AU - Ferreira Pires, Luis

    AU - Lopes de Souza, Wanderley

    AU - Moron, Célio Estevan

    PY - 2001/8/15

    Y1 - 2001/8/15

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

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

    KW - METIS-204031

    KW - IR-37117

    U2 - 10.1109/MASCOT.2001.948848

    DO - 10.1109/MASCOT.2001.948848

    M3 - Conference contribution

    SN - 0-7695-1315-8

    SP - 7

    EP - 14

    BT - MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems

    A2 - Das, S.R.

    A2 - Nicol, D.

    A2 - Perrone, F.

    PB - University of Cincinatti

    ER -

    Guareis de farias C, Ferreira Pires L, Lopes de Souza W, Moron CE. Specification and Validation of a Real-Time Parallel Kernel using LOTOS. In Das SR, Nicol D, Perrone F, editors, MASCOTS 2001, Proceedings Ninth International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. University of Cincinatti. 2001. p. 7-14 https://doi.org/10.1109/MASCOT.2001.948848