Extending specification patterns for verification of parametric traces
| Autor: | Yoann Blein, Roland Groz, Yves Ledru, Lydie du-Bousquet |
|---|---|
| Přispěvatelé: | Validation de Systèmes, Composants et Objets logiciels (VASCO), Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), ANR-15-CE25-0010,MODMED,MODèles pour la Vérification de Systèmes Cyber-Physiques MEDicaux(2015) |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
Semantics (computer science)
Computer science 0102 computer and information sciences 02 engineering and technology [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Semantics computer.software_genre 01 natural sciences CCS CONCEPTS • Software and its engineering → Specification languages Temporal Specification 0202 electrical engineering electronic engineering information engineering Parametric Events TRACE (psycholinguistics) computer.programming_language Syntax (programming languages) Programming language Trace Analysis Runtime verification 020207 software engineering Specification language Formal software verification JSON 010201 computation theory & mathematics Design rationale KEYWORDS Runtime Verification computer |
| Zdroj: | the 6th Conference on Formal Methods in Software Engineering (FormaliSE'18) the 6th Conference on Formal Methods in Software Engineering (FormaliSE'18), Jun 2018, Gothenburg, Sweden. pp.10-19, ⟨10.1145/3193992.3193998⟩ FormaliSE@ICSE |
| DOI: | 10.1145/3193992.3193998⟩ |
| Popis: | International audience; This article proposes a temporal and parametric specification language (ParTraP) developed for the verification of execution traces. The language extends specification patterns with nested scopes, real-time and first-order quantification over the data inside a JSON trace, while remaining pragmatic. Its design was directed by a case study in the medical field (computer aided surgery). The paper briefly presents the case study and details the design rationale, syntax and semantics of the language. The language has been implemented and several properties have been successfully evaluated over a corpus of 100 surgery traces. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|