Embedded software analysis with MOTOR

Joost-Pieter Katoen, Henrik Bohnenkamp, Ric Klaren, Holger Hermanns

    Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

    2 Citations (Scopus)
    68 Downloads (Pure)

    Abstract

    This paper surveys the language Modest, a Modelling and Description language for Stochastic and Timed systems, and its accompanying tool-environment MOTOR. The language and tool are aimed to support the modular description and analysis of reactive systems while covering both functional and non-functional system aspects such as hard and soft real-time, and quality-of-service aspects. As an illustrative example, the modeling and analysis of a device-absence detecting protocol in plug-and-play networks is described and is shown to exhibit some undesired behaviour.
    Original languageEnglish
    Title of host publicationFormal Methods for the Design of Real-Time Systems
    Subtitle of host publicationInternational School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004. Revised Lectures
    EditorsMarco Bernardo, Flavio Corradini
    PublisherSpringer
    Pages268-293
    Number of pages26
    ISBN (Electronic)978-3-540-30080-9
    ISBN (Print)978-3-540-23068-8-7
    DOIs
    Publication statusPublished - 2004
    EventInternational School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004 - Bertinoro, Italy
    Duration: 13 Sep 200418 Sep 2004

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume3185
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    ConferenceInternational School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004
    Abbreviated titleSFM-RT
    CountryItaly
    CityBertinoro
    Period13/09/0418/09/04

    Keywords

    • FMT-PM: PROBABILISTIC METHODS
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-TOOLS
    • Model checker
    • Operational semantics
    • Overlay networks
    • Critical section
    • Mutual exclusion

    Fingerprint Dive into the research topics of 'Embedded software analysis with MOTOR'. Together they form a unique fingerprint.

  • Cite this

    Katoen, J-P., Bohnenkamp, H., Klaren, R., & Hermanns, H. (2004). Embedded software analysis with MOTOR. In M. Bernardo, & F. Corradini (Eds.), Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004. Revised Lectures (pp. 268-293). (Lecture Notes in Computer Science; Vol. 3185). Springer. https://doi.org/10.1007/b110123