Incremental methods for checking real-time consistency
| Autor: | David Mentré, Nicolas Markey, Ocan Sankur, Reiya Noguchi, Thierry Jéron |
|---|---|
| Přispěvatelé: | SUpervision of large MOdular and distributed systems (SUMO), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Mitsubishi Electric R&D Centre Europe [France] (MERCE-France), Mitsubishi Electric [France], ANR-18-CE40-0015,TickTac,Techniques et outils efficaces pour la vérification et synthèse des systèmes temps-réels(2018), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
050101 languages & linguistics
Theoretical computer science Requirements engineering Process (engineering) Computer science 05 social sciences Computer Science - Formal Languages and Automata Theory 02 engineering and technology [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Automaton Consistency (database systems) Computer Science - Software Engineering Time consistency 0202 electrical engineering electronic engineering information engineering Key (cryptography) 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Formal verification Implementation |
| Zdroj: | FORMATS 2020-18th International Conference on Formal Modeling and Analysis of Timed Systems FORMATS 2020-18th International Conference on Formal Modeling and Analysis of Timed Systems, Sep 2020, Vienne, Austria. pp.1-18 Lecture Notes in Computer Science ISBN: 9783030576271 FORMATS |
| Popis: | Requirements engineering is a key phase in the development process. Ensuring that requirements are consistent is essential so that they do not conflict and admit implementations. We consider the formal verification of rt-consistency, which imposes that the inevitability of definitive errors of a requirement should be anticipated, and that of partial consistency, which was recently introduced as a more effective check. We generalize and formalize both notions for discrete-time timed automata, develop three incremental algorithms, and present experimental results. Comment: 18 pages, published in Formats 2020 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|