Verification and analysis of domain-specific models of physical characteristics in embedded control software

Arjan de Roo, Hasan Sözer, Mehmet Aksit

    Research output: Contribution to journalArticleAcademicpeer-review

    4 Citations (Scopus)
    23 Downloads (Pure)

    Abstract

    Context: A considerable portion of the software systems today are adopted in the embedded control domain. Embedded control software deals with controlling a physical system, and as such models of physical characteristics become part of the embedded control software. Objective: Due to the evolution of system properties and increasing complexity, faults can be left undetected in these models of physical characteristics. Therefore, their accuracy must be verified at runtime. Traditional runtime verification techniques that are based on states/events in software execution are inadequate in this case. The behavior suggested by models of physical characteristics cannot be mapped to behavioral properties of software. Moreover, implementation in a general-purpose programming language makes these models hard to locate and verify. Therefore, this paper proposes a novel approach to perform runtime verification of models of physical characteristics in embedded control software. Method: The development of an approach for runtime verification of models of physical characteristics and the application of the approach to two industrial case studies from the printing systems domain. Results: This paper presents a novel approach to specify models of physical characteristics using a domain-specific language, to define monitors that detect inconsistencies by exploiting redundancy in these models, and to realize these monitors using an aspect-oriented approach. We complement runtime verification with static analysis to verify the composition of domain-specific models with the control software written in a general-purpose language. Conclusions: The presented approach enables runtime verification of implemented models of physical characteristics to detect inconsistencies in these models, as well as broken hardware components and wear and tear of hardware in the physical system. The application of declarative aspect-oriented techniques to realize runtime verification monitors increases modularity and provides the ability to statically verify this realization. The complementary static and runtime verification techniques increase the reliability of embedded control software.
    Original languageUndefined
    Pages (from-to)1432-1453
    Number of pages22
    JournalInformation and software technology
    Volume54
    Issue number12
    DOIs
    Publication statusPublished - Dec 2012

    Keywords

    • EWI-22363
    • METIS-296108
    • IR-83363
    • Runtime verification
    • Domain-specific languages
    • Control software
    • Embedded Systems
    • Aspect-Oriented Software Development

    Cite this

    @article{2c80ee736f034e86bbfc3e8be37bd915,
    title = "Verification and analysis of domain-specific models of physical characteristics in embedded control software",
    abstract = "Context: A considerable portion of the software systems today are adopted in the embedded control domain. Embedded control software deals with controlling a physical system, and as such models of physical characteristics become part of the embedded control software. Objective: Due to the evolution of system properties and increasing complexity, faults can be left undetected in these models of physical characteristics. Therefore, their accuracy must be verified at runtime. Traditional runtime verification techniques that are based on states/events in software execution are inadequate in this case. The behavior suggested by models of physical characteristics cannot be mapped to behavioral properties of software. Moreover, implementation in a general-purpose programming language makes these models hard to locate and verify. Therefore, this paper proposes a novel approach to perform runtime verification of models of physical characteristics in embedded control software. Method: The development of an approach for runtime verification of models of physical characteristics and the application of the approach to two industrial case studies from the printing systems domain. Results: This paper presents a novel approach to specify models of physical characteristics using a domain-specific language, to define monitors that detect inconsistencies by exploiting redundancy in these models, and to realize these monitors using an aspect-oriented approach. We complement runtime verification with static analysis to verify the composition of domain-specific models with the control software written in a general-purpose language. Conclusions: The presented approach enables runtime verification of implemented models of physical characteristics to detect inconsistencies in these models, as well as broken hardware components and wear and tear of hardware in the physical system. The application of declarative aspect-oriented techniques to realize runtime verification monitors increases modularity and provides the ability to statically verify this realization. The complementary static and runtime verification techniques increase the reliability of embedded control software.",
    keywords = "EWI-22363, METIS-296108, IR-83363, Runtime verification, Domain-specific languages, Control software, Embedded Systems, Aspect-Oriented Software Development",
    author = "{de Roo}, Arjan and Hasan S{\"o}zer and Mehmet Aksit",
    year = "2012",
    month = "12",
    doi = "10.1016/j.infsof.2012.07.005",
    language = "Undefined",
    volume = "54",
    pages = "1432--1453",
    journal = "Information and software technology",
    issn = "0950-5849",
    publisher = "Elsevier",
    number = "12",

    }

    Verification and analysis of domain-specific models of physical characteristics in embedded control software. / de Roo, Arjan; Sözer, Hasan; Aksit, Mehmet.

    In: Information and software technology, Vol. 54, No. 12, 12.2012, p. 1432-1453.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Verification and analysis of domain-specific models of physical characteristics in embedded control software

    AU - de Roo, Arjan

    AU - Sözer, Hasan

    AU - Aksit, Mehmet

    PY - 2012/12

    Y1 - 2012/12

    N2 - Context: A considerable portion of the software systems today are adopted in the embedded control domain. Embedded control software deals with controlling a physical system, and as such models of physical characteristics become part of the embedded control software. Objective: Due to the evolution of system properties and increasing complexity, faults can be left undetected in these models of physical characteristics. Therefore, their accuracy must be verified at runtime. Traditional runtime verification techniques that are based on states/events in software execution are inadequate in this case. The behavior suggested by models of physical characteristics cannot be mapped to behavioral properties of software. Moreover, implementation in a general-purpose programming language makes these models hard to locate and verify. Therefore, this paper proposes a novel approach to perform runtime verification of models of physical characteristics in embedded control software. Method: The development of an approach for runtime verification of models of physical characteristics and the application of the approach to two industrial case studies from the printing systems domain. Results: This paper presents a novel approach to specify models of physical characteristics using a domain-specific language, to define monitors that detect inconsistencies by exploiting redundancy in these models, and to realize these monitors using an aspect-oriented approach. We complement runtime verification with static analysis to verify the composition of domain-specific models with the control software written in a general-purpose language. Conclusions: The presented approach enables runtime verification of implemented models of physical characteristics to detect inconsistencies in these models, as well as broken hardware components and wear and tear of hardware in the physical system. The application of declarative aspect-oriented techniques to realize runtime verification monitors increases modularity and provides the ability to statically verify this realization. The complementary static and runtime verification techniques increase the reliability of embedded control software.

    AB - Context: A considerable portion of the software systems today are adopted in the embedded control domain. Embedded control software deals with controlling a physical system, and as such models of physical characteristics become part of the embedded control software. Objective: Due to the evolution of system properties and increasing complexity, faults can be left undetected in these models of physical characteristics. Therefore, their accuracy must be verified at runtime. Traditional runtime verification techniques that are based on states/events in software execution are inadequate in this case. The behavior suggested by models of physical characteristics cannot be mapped to behavioral properties of software. Moreover, implementation in a general-purpose programming language makes these models hard to locate and verify. Therefore, this paper proposes a novel approach to perform runtime verification of models of physical characteristics in embedded control software. Method: The development of an approach for runtime verification of models of physical characteristics and the application of the approach to two industrial case studies from the printing systems domain. Results: This paper presents a novel approach to specify models of physical characteristics using a domain-specific language, to define monitors that detect inconsistencies by exploiting redundancy in these models, and to realize these monitors using an aspect-oriented approach. We complement runtime verification with static analysis to verify the composition of domain-specific models with the control software written in a general-purpose language. Conclusions: The presented approach enables runtime verification of implemented models of physical characteristics to detect inconsistencies in these models, as well as broken hardware components and wear and tear of hardware in the physical system. The application of declarative aspect-oriented techniques to realize runtime verification monitors increases modularity and provides the ability to statically verify this realization. The complementary static and runtime verification techniques increase the reliability of embedded control software.

    KW - EWI-22363

    KW - METIS-296108

    KW - IR-83363

    KW - Runtime verification

    KW - Domain-specific languages

    KW - Control software

    KW - Embedded Systems

    KW - Aspect-Oriented Software Development

    U2 - 10.1016/j.infsof.2012.07.005

    DO - 10.1016/j.infsof.2012.07.005

    M3 - Article

    VL - 54

    SP - 1432

    EP - 1453

    JO - Information and software technology

    JF - Information and software technology

    SN - 0950-5849

    IS - 12

    ER -