A Model for Industrial Real-Time Systems

Md Tawhid Bin Waez, Andrzej Wasowski, Juergen Dingel, Karen Rudie

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    Abstract

    Introducing automated formal methods for large industrial real-time systems is an important research challenge. We propose timed process automata (TPA) for modeling and analysis of time-critical systems which can be open, hierarchical, and dynamic. The model offers two essential features for large industrial systems: (i) compositional modeling with reusable designs for different contexts, and (ii) an automated state-space reduction technique. Timed process automata model dynamic networks of continuous-time communicating control processes which can activate other processes. We show how to automatically establish safety and reachability properties of TPA by reduction to solving timed games. To mitigate the state-space explosion problem, an automated state-space reduction technique using compositional reasoning and aggressive abstractions is also proposed.
    Original languageEnglish
    Title of host publicationVerification, Model Checking, and Abstract Interpretation : 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings.
    EditorsDeepak D'Souza, Akash Lal, Kim Guldstrand Larsen
    Volume8931
    PublisherSpringer
    Publication date2015
    Pages153-171
    ISBN (Print)978-3-662-46080-1
    DOIs
    Publication statusPublished - 2015
    SeriesLecture Notes in Computer Science
    ISSN0302-9743

    Keywords

    • Automated formal methods
    • Timed process automata
    • State-space reduction
    • Compositional modeling
    • Timed games

    Fingerprint

    Dive into the research topics of 'A Model for Industrial Real-Time Systems'. Together they form a unique fingerprint.

    Cite this