A compositional monitoring framework for hard real-time systems
| Autor: | Luis Miguel Pinho, André de Matos Pedro, Jorge Sousa Pinto, David Pereira |
|---|---|
| Přispěvatelé: | Universidade do Minho |
| Jazyk: | angličtina |
| Rok vydání: | 2014 |
| Předmět: |
Correctness
Science & Technology Computer science business.industry Distributed computing Runtime verification Real-time computing Response time 020207 software engineering Ciências Naturais::Ciências da Computação e da Informação 02 engineering and technology 020202 computer hardware & architecture Monitors Software Criticality Embedded system Real-time Systems 0202 electrical engineering electronic engineering information engineering Temporal logic Isolation (database systems) business Engenharia e Tecnologia::Engenharia Eletrotécnica Eletrónica e Informática |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319061993 NASA Formal Methods |
| Popis: | Runtime Monitoring of hard real-time embedded systems is a promising technique for ensuring that a running system respects timing constraints, possibly combined with faults originated by the software and/or hardware. This is particularly important when we have real-time embedded systems made of several components that must combine different levels of criticality, and different levels of correctness requirements. This paper introduces a compositional monitoring framework coupled with guarantees that include time isolation and the response time of a monitor for a predicted violation. The kind of monitors that we propose are automatically generated by synthesizing logic formulas of a timed temporal logic, and their correctness is ensured by construction. This work was partially supported by National Funds through FCT (Portuguese Foundation for Science and Technology) and by ERDF (European Regional Development Fund) through COMPETE (Operational Programme ’Thematic Factors of Competitiveness’), within projects Ref. FCOMP-01-0124-FEDER-022701 (CISTER), FCOMP-01-0124- FEDER-015006 (VIPCORE) and FCOMP-01-0124-FEDER-020486 (AVIACC). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|