25 results on '"property specification"'
Search Results
2. TimeLine Depiction: an approach to graphical notation for supporting temporal property specification.
- Author
-
Sin, Chun-Ok and Kim, Yong-Sok
- Abstract
The finite-state verification techniques such as model checking allow for automated checking whether system model described with automata satisfy temporal properties, or not. The temporal properties should be typically specified in temporal logic formulae, which is a difficult task for programmers who aren't verification experts. Therefore, there is a few of research to propose description languages with which non-experts can accurately express temporal requirements on system's behaviors and the methods transforming them automatically into temporal property specification of particular model checker. We analyzed various researches aimed at the construction of property specifications, that is, machine translation from natural language to temporal logical formula, property specification pattern and graphical scenarios for specifying property, and so on. Based on the analysis, in this paper, we present a visual language called TimeLineDepic, which is a user-friendly graphical notation for temporal property description and whose expressive power is same as other languages. And we propose a method to transform TimeLineDepic to buchi automata (never claim) and insert it in promela-based model for model checker SPIN. [ABSTRACT FROM AUTHOR]
- Published
- 2023
- Full Text
- View/download PDF
3. Sibilla: A tool for reasoning about collective systems.
- Author
-
Del Giudice, Nicola, Matteucci, Lorenzo, Quadrini, Michela, Rehman, Aniqa, and Loreti, Michele
- Subjects
- *
CLOUD computing , *QUANTITATIVE research - Abstract
Formal approaches and tools have been defined, implemented and successfully applied to support the design and development of Collective Adaptive Systems. These tools are highly specialised in their fields, and their integration requires an effort. In this paper, we introduce Sibilla , a Java modular tool that facilitates the integration of multiple specification languages for supporting quantitative analysis of systems. After a description of the general architecture of Sibilla , the main features of the tool are discussed via simple examples. • Sibilla is a modular framework for specification and analysis of Collective Systems. • Sibilla integrates tools for simulation and statistical analysis/model-checking. • Sibilla simplifies the integration of new languages and tools. • Sibilla can be easily deployed on multiple platforms and Cloud Services. [ABSTRACT FROM AUTHOR]
- Published
- 2024
- Full Text
- View/download PDF
4. Generic Methodology for Formal Verification of UML Models.
- Author
-
Kochaleema, K. H. and Kumar, G. Santhosh
- Subjects
UNIFIED modeling language ,COMPUTER software development - Abstract
This paper discusses a Unified Modelling Language (UML) based formal verification methodology for early error detection in the model-based software development cycle. Our approach proposes a UML-based formal verification process utilising functional and behavioural modelling artifacts of UML. It reinforces these artifacts with formal model transition and property verification. The main contribution is a UML to Labelled Transition System (LTS) Translator application that automatically converts UML Statecharts to formal models. Property specifications are derived from system requirements and corresponding Computational Tree Logic (CTL)/Linear Temporal Logic (LTL) model checking procedure verifies property entailment in LTS. With its ability to verify CTL and LTL specifications, the methodology becomes generic for verifying all types of embedded system behaviours. The steep learning curve associated with formal methods is avoided through the automatic formal model generation and thus reduces the reluctance of using formal methods in software development projects. A case study of an embedded controller used in military applications validates the methodology. It establishes how the methodology finds its use in verifying the correctness and consistency of UML models before implementation. [ABSTRACT FROM AUTHOR]
- Published
- 2022
- Full Text
- View/download PDF
5. A Research Landscape on Formal Verification of Software Architecture Descriptions
- Author
-
Camila Araujo, Everton Cavalcante, Thais Batista, Marcel Oliveira, and Flavio Oquendo
- Subjects
Architecture description ,formal verification ,property specification ,software architectures ,systematic mapping ,Electrical engineering. Electronics. Nuclear engineering ,TK1-9971 - Abstract
One of the many different purposes of software architecture descriptions is contributing to an early analysis of the architecture with respect to quality attributes. The critical nature of many software systems calls for formal approaches aiming at precisely verifying if their designed architectures can meet important properties such as consistency, completeness, and correctness. In this context, it is worthwhile investigating the role of architecture descriptions to support the formal verification of software architectures to ensure their quality, as well as how such a process happens and is supported by existing languages and verification tools. To evaluate the research landscape on this subject, we have carried out a systematic mapping study in which we collected and analyzed studies available at the literature on formal verification of architecture descriptions. This work contributes with (i) a structured overview and taxonomy of the current state of the art on this topic and (ii) the elicitation of important issues to be addressed in future research.
- Published
- 2019
- Full Text
- View/download PDF
6. A MORE FAITHFUL FORMAL DEFINITION OF THE DESIRED PROPERTY FOR DISTRIBUTED SNAPSHOT ALGORITHMS TO MODEL CHECK THE PROPERTY.
- Author
-
Ha Thi Thu DOAN and Kazuhiro OGATA
- Subjects
DEFINITIONS ,SYSTEMS software - Abstract
The first distributed snapshot algorithm was invented by Chandy and Lamport: Chandy-Lamport distributed snapshot algorithm (CLDSA). Distributed snapshot algorithms are crucial components to make distributed systems fault tol- erant. Such algorithms are extremely important because many modern key software systems are in the form of distributed systems and should be fault tolerant. There are at least two desired properties such algorithms should satisfy: 1) the distributed snapshot reachability property (called the DSR property) and 2) the ability to run concurrently with, but not alter, an underlying distributed system (UDS). This paper identifies subtle errors in a paper on formalization of the DSR property and shows how to correct them. We give a more faithful formal definition of the DSR property; the definition involves two state machines - one state machine M
UDS that formalizes a UDS and the other MCLDSA that formalizes the UDS on which CLDSA is superimposed (UDS-CLDSA) - and can be used to more precise model checking of the DSR property for CLDSA. We also prove a theorem on equivalence of our new definition and an existing one that only involves MCLDSA to guarantee the validity of the existing model checking approach. Moreover, we prove the second property, namely that CLDSA does not alter the behaviors of UDS. [ABSTRACT FROM AUTHOR]- Published
- 2019
- Full Text
- View/download PDF
7. DaProS: A Data Property Specification Tool to Capture Scientific Sensor Data Properties
- Author
-
Gallegos, Irbis, Gates, Ann Q., Tweedie, Craig, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Trujillo, Juan, editor, Dobbie, Gillian, editor, Kangassalo, Hannu, editor, Hartmann, Sven, editor, Kirchberg, Markus, editor, Rossi, Matti, editor, Reinhartz-Berger, Iris, editor, Zimányi, Esteban, editor, and Frasincar, Flavius, editor
- Published
- 2010
- Full Text
- View/download PDF
8. Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial)
- Author
-
Foster, Harry, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Gupta, Aarti, editor, and Malik, Sharad, editor
- Published
- 2008
- Full Text
- View/download PDF
9. Joint Structural and Temporal Property Specification Using Timed Story Scenario Diagrams
- Author
-
Klein, Florian, Giese, Holger, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Rangan, C. Pandu, editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Dwyer, Matthew B., editor, and Lopes, Antónia, editor
- Published
- 2007
- Full Text
- View/download PDF
10. On a Temporal Logic for Object-Based Systems
- Author
-
Distefano, Dino, Katoen, Joost-Pieter, Rensink, Arend, Smith, Scott F., editor, and Talcott, Carolyn L., editor
- Published
- 2000
- Full Text
- View/download PDF
11. Property specification, process verification, and reporting – A case study with vehicle-commissioning processes.
- Author
-
Mrasek, Richard, Mülle, Jutta, Böhm, Klemens, Becker, Michael, and Allmann, Christian
- Subjects
- *
AUTOMOBILE industry , *PETRI nets , *BUSINESS process management , *WORKFLOW management systems , *MANUFACTURING processes , *EMPIRICAL research ,MOTOR vehicle testing - Abstract
Testing in the automotive industry is supposed to guarantee that vehicles are shipped without any flaw. Respective processes are complex, due to the variety of components and electronic devices in modern vehicles. To achieve error-free processes, their formal analysis is required. Specifying and maintaining properties the processes must satisfy in a user-friendly way is a core requirement on any verification system. We have observed that there are few property templates that testing processes must adhere to, and we describe these templates. They depend on the context of the processes, e.g., the components of the vehicle or testing stations. We have developed a framework that instantiates the templates of properties at verification time and then verifies the process against these instances. To allow an automatic verification we develop a transformation of the commissioning process to a Petri net. Using a novel approach, we are able to report the found violations to the user in a user-friendly way. Our empirical evaluation with the industrial partner has shown that our framework does detect property violations in processes. From expert interviews we conclude that our framework is user-friendly and well suited to operate in a real production environment. [ABSTRACT FROM AUTHOR]
- Published
- 2016
- Full Text
- View/download PDF
12. TRAP: trace runtime analysis of properties
- Author
-
Yue, Daian, Joloboff, Vania, and Mallet, Frédéric
- Published
- 2019
- Full Text
- View/download PDF
13. TRAP: trace runtime analysis of properties
- Author
-
Daian Yue, Frédéric Mallet, Vania Joloboff, Shanghai Key Laboratory of Trustworthy Computing, East China Normal University [Shangaï] (ECNU), Tim, Events and Architectures (TEA), 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 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 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)-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), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Bull SAS (Bull), Bull SAS, COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA), Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), This work was supported by the Sino-EuropeanLIAMA Laboratory and by the INRIA Sophia Antipolis Research Center., 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 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), Université Nice Sophia Antipolis (1965 - 2019) (UNS), and COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS)
- Subjects
Domain-specific language ,trace analysis ,General Computer Science ,virtual prototyping ,Computer science ,02 engineering and technology ,computer.software_genre ,property specification ,Theoretical Computer Science ,logical clocks ,Virtual prototyîng ,0202 electrical engineering, electronic engineering, information engineering ,ComputingMilieux_MISCELLANEOUS ,computer.programming_language ,TRACE (psycholinguistics) ,Programming language ,Runtime verification ,020207 software engineering ,Specification language ,Data structure ,Embedded software ,Digital subscriber line ,020201 artificial intelligence & image processing ,Property Specification Language ,[INFO.INFO-ES]Computer Science [cs]/Embedded Systems ,computer ,Simulation - Abstract
We present a method and a tool for the verification of causal and temporal properties for embedded systems. We analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware and embedded software. The main originality lies in the use of logical clocks to abstract away irrelevant information from the trace. We propose a model-based approach that relies on domain specific languages (DSL). A first DSL, called TISL (trace item specification language), captures the relevant data structures. A second DSL, called STML (simulation trace mapping language), abstracts the simulation raw data into logical clocks, abstracting simulation data into relevant observation probes and thus reducing the trace streams size. The third DSL, called TPSL, defines a set of behavioral patterns that include widely used temporal properties. This is meant for users who are not familiar with temporal logics. Each pattern is transformed into an automata. All the automata are executed concurrently and each one raises an error if and when the related TPSL property is violated. The contribution is the integration of this pattern-based property specification language into the SimSoC virtual prototyping framework without requiring to recompile all the simulation models when the properties evolve. We illustrate our approach with experiments that show the possibility to use multi-core platforms to parallelize the simulation and verification processes, thus reducing the verification time.
- Published
- 2020
14. A More Faithful Formal Definition of the Desired Property for Distributed Snapshot Algorithms to Model Check the Property
- Author
-
Ha Thi Thu Doan and Kazuhiro Ogata
- Subjects
Model checking ,68N30 ,Finite-state machine ,Computer science ,General Engineering ,Fault tolerance ,Snapshot algorithm ,property specification ,model checking ,state machine ,Reachability ,Snapshot (computer storage) ,Software system ,Distributed snapshot algorithm ,Algorithm ,Formal description ,reachability - Abstract
The first distributed snapshot algorithm was invented by Chandy and Lamport: Chandy-Lamport distributed snapshot algorithm (CLDSA). Distributed snapshot algorithms are crucial components to make distributed systems fault tolerant. Such algorithms are extremely important because many modern key software systems are in the form of distributed systems and should be fault tolerant. There are at least two desired properties such algorithms should satisfy: 1) the distributed snapshot reachability property (called the DSR property) and 2) the ability to run concurrently with, but not alter, an underlying distributed system (UDS). This paper identifies subtle errors in a paper on formalization of the DSR property and shows how to correct them. We give a more faithful formal definition of the DSR property; the definition involves two state machines - one state machine M_UDS that formalizes a UDS and the other M_CLDSA that formalizes the UDS on which CLDSA is superimposed (UDS-CLDSA) - and can be used to more precise model checking of the DSR property for CLDSA. We also prove a theorem on equivalence of our new definition and an existing one that only involves M_CLDSA to guarantee the validity of the existing model checking approach. Moreover, we prove the second property, namely that CLDSA does not alter the behaviors of UDS.
- Published
- 2020
15. Use Case Maps as a property specification language.
- Author
-
Hassine, Jameleddine, Rilling, Juergen, and Dssouli, Rachida
- Subjects
- *
SYSTEMS software , *USE cases (Systems engineering) , *TEMPORAL databases , *COMPUTER input-output equipment , *LOGIC programming - Abstract
Although a significant body of research in the area of formal verification and model checking tools of software and hardware systems exists, the acceptance of these tools by industry and end-users is rather limited. Beside the technical problem of state space explosion, one of the main reasons for this limited acceptance is the unfamiliarity of users with the required specification notation. Requirements have to be typically expressed as temporal logic formalisms and notations. Property specification patterns were successfully introduced to bridge this gap between users and model checking tools. They also enable non-experts to write formal specifications that can be used for automatic model checking. In this paper, we propose an abstract high level pattern-based approach to the description of property specifications based on Use Case Maps (UCM). We present a set of commonly used properties with their specifications that are described in terms of occurrence, ordering and temporal scopes of actions. Furthermore, our approach also supports the description of properties with respect to their architectural scope. We provide a mapping of our UCM property specification patterns in terms of CTL, TCTL and Architectural TCTL (ArTCTL), an extension to TCTL, introduced in this research that provides temporal logics with architectural scopes. We illustrate the use of our pattern system for requirement specifications of an IP Header compression feature. [ABSTRACT FROM AUTHOR]
- Published
- 2009
- Full Text
- View/download PDF
16. A NEW APPROACH TO VERIFY STATECHART SPECIFICATIONS FOR REACTIVE SYSTEMS.
- Author
-
MO, YUCHANG and YANG, XINMIN
- Subjects
TELECOMMUNICATION ,EMBEDDED computer systems ,ELECTRONIC controllers ,AVIONICS ,COMPUTER networks - Abstract
The application domain, such as communication networks and embedded controllers for telephony, automobiles, trains and avionics systems, requires very high quality reactive systems, so an important phase in the development of reactive systems is the verification of their conceptual models before implementation. Normally in the requirement analysis phase, system property can be represented as an input and output labeled transition system (IOLTS), which is a transition system labeled by inputs and outputs between the system and the environment. This paper describes an attempt to propose an approach to verify Statechart specifications for reactive systems given IOLTS property specifications. We develop a suitable semantics model — observable semantics, an abstract semantics model only which describes outside observable behavior and suffers from less state explosion problem by reducing infinite or large state spaces to small ones. Then we propose two methods to verify the conformance between a given IOLTS property specification and a Statechart specification: two-phase verification and on-the-fly verification. Compared with two-phase verification, on-the-fly verification needs less storage and computation-time, especially when the target Statechart specification is very large or likely to have many errors. [ABSTRACT FROM AUTHOR]
- Published
- 2008
- Full Text
- View/download PDF
17. GENERATING PROPERTIES FOR RUNTIME MONITORING FROM SOFTWARE SPECIFICATION PATTERNS.
- Author
-
MONDRAGON, OSCAR A., GATES, ANN Q., ROACH, STEVE, MENDOZA, HUMBERTO, and SOKOLSKY, OLEG
- Subjects
PROGRAMMING languages ,ELECTRONIC systems ,JAVA programming language ,ELECTRONIC data processing ,ALGORITHMS - Abstract
This paper presents an approach to support run-time verification of software systems that combines two existing tools, Prospec and Java-MaC, into a single framework. Prospec can be used to clarify natural language specifications for sequential, concurrent, and nondeterministic behavior. In addition, Prospec assists the user in reading, writing, and understanding formal specifications through the use of property patterns and visual abstractions. Prospec automatically generates specifications written in Future Interval Logic (FIL). Java-MaC monitors Java programs at runtime to ensure adherence to a set of formally specified properties. Safety properties of a program are specified in the formal language Meta-Event Definition Language (MEDL). Java-MaC generates runtime components from specifications. The components are used to instrument the target program and determine whether the execution of the program violates any of the safety properties. This paper describes an algorithm for translating FIL formulas into MEDL formulas. It provides the transformation rules used by this algorithm, and it demonstrates the general correctness of the translation. [ABSTRACT FROM AUTHOR]
- Published
- 2007
- Full Text
- View/download PDF
18. System Resource Utilization Analysis based on Model Checking Method.
- Author
-
Ki-Seok Bang, Hyun-Wook Jin, Chuck-Yoo, and Jin-Young Choi
- Subjects
FORMAL methods (Computer science) ,COMPUTER systems ,SYSTEMS design ,ELECTRONIC data processing ,SYSTEM analysis - Abstract
Model checking method is a widely used formal method for proving whether or not a given model satisfies properties, and for producing counter examples if the model does not satisfy properties. In this paper, we show model checking methods can be used for resource utilization analysis of systems. We specify system utilization properties using temporal logic called LTL, and find a bottleneck of system performance using model checking. [ABSTRACT FROM AUTHOR]
- Published
- 2005
19. SUPPORTING ELICITATION AND SPECIFICATION OF SOFTWARE PROPERTIES THROUGH PATTERNS AND COMPOSITE PROPOSITIONS.
- Author
-
Mondragón, Oscar A. and Gates, Ann Q.
- Subjects
TECHNICAL specifications ,COMPUTER software ,PROPOSITION (Logic) ,SOFTWARE validation ,SOFTWARE engineering ,LOGIC - Abstract
Prospec is a tool that assists practitioners in the elicitation and specification of system properties. Practitioners are guided by questions, definitions, and graphics. Prospec introduces the use of composite propositions to identify intended behavior when multiple conditions or events are considered. Multiple conditions or events may represent behavior such as sequences, concurrency, and non-determinism and may define the boundaries of scopes or type of patterns. Prospec is built upon the Specification Pattern System. The tool assists the analyst in making informed decisions about aspects of a specification that may have multiple interpretations. The end product of the tool is a formal specification in Future Interval Logic, Linear Temporal Logic, or Meta Event Definition Language. [ABSTRACT FROM AUTHOR]
- Published
- 2004
20. TRAP: trace runtime analysis of properties.
- Author
-
Yue, Daian, Joloboff, Vania, and Mallet, Frédéric
- Abstract
We present a method and a tool for the verification of causal and temporal properties for embedded systems. We analyze trace streams resulting from the execution of virtual prototypes that combine simulated hardware and embedded software. The main originality lies in the use of logical clocks to abstract away irrelevant information from the trace. We propose a model-based approach that relies on domain specific languages (DSL). A first DSL, called TISL (trace item specification language), captures the relevant data structures. A second DSL, called STML (simulation trace mapping language), abstracts the simulation raw data into logical clocks, abstracting simulation data into relevant observation probes and thus reducing the trace streams size. The third DSL, called TPSL, defines a set of behavioral patterns that include widely used temporal properties. This is meant for users who are not familiar with temporal logics. Each pattern is transformed into an automata. All the automata are executed concurrently and each one raises an error if and when the related TPSL property is violated. The contribution is the integration of this pattern-based property specification language into the SimSoC virtual prototyping framework without requiring to recompile all the simulation models when the properties evolve. We illustrate our approach with experiments that show the possibility to use multi-core platforms to parallelize the simulation and verification processes, thus reducing the verification time. [ABSTRACT FROM AUTHOR]
- Published
- 2020
- Full Text
- View/download PDF
21. Flexible Runtime Verification Based On Logical Clock Constraints
- Author
-
Vania Joloboff, Daian Yue, Frédéric Mallet, Tim, Events and Architectures (TEA), 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)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-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)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-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)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), East China Normal University [Shangaï] (ECNU), Models and methods of analysis and optimization for systems with real-time and embedding constraints (AOSTE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA), INRIA, ECNU, ENS Rennes, ECSI, East China Normal University - Equipe Associée Inria FCPMS, Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-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 Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-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)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-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)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Inria Rennes – Bretagne Atlantique
- Subjects
trace analysis ,virtual prototyping ,Computer science ,Distributed computing ,media_common.quotation_subject ,0102 computer and information sciences ,02 engineering and technology ,Parallel computing ,01 natural sciences ,property specification ,0202 electrical engineering, electronic engineering, information engineering ,Logical clock ,model driven engineering ,computer.programming_language ,TRACE (psycholinguistics) ,media_common ,clock constraint specification language ,Runtime verification ,020207 software engineering ,simulation ,debugging ,Embedded software ,Debugging ,010201 computation theory & mathematics ,Property Specification Language ,[INFO.INFO-ES]Computer Science [cs]/Embedded Systems ,Model-driven architecture ,computer ,Virtual prototyping - Abstract
International audience; We present in this paper a method and tool for the verification of causal and temporal properties of embedded systems, by analyzing the trace streams resulting from virtual prototypes that combines simulated hardware and embedded software. The proposed method makes it possible to analyze different kinds of properties without rebuilding the simulation models. Logical clocks are used to identify relevant points to put observation probes and thus also reducing the trace streams size. We propose a property specification language, called PSML, and based on behavioral patterns that does not require knowledge of temporal logics. From a given PSML specification, simulation is instrumented to generate a trace and the code is dynamically loaded by the simulator. The resulting trace stream is analyzed by parallel automata generated from the specification. The experiments, developed over the SimSoC virtual prototyping framework, show flexibility, possibility of using multi-core platforms to parallelize simulation and verification, providing fast results.
- Published
- 2016
22. Modèles orientés utilisateurs pour la vérification formelle en contexte industriel
- Author
-
Raji, Amine, Dhaussy, Philippe, Laboratoire d'Informatique des Systèmes Complexes (LISYC), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Brest (UBO)-Institut Brestois du Numérique et des Mathématiques (IBNM), Université de Brest (UBO)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne), Département STIC [Brest] (STIC), École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne), and Billon-Coat, Annick
- Subjects
context models ,Formal methods ,[SHS.INFO]Humanities and Social Sciences/Library and information sciences ,[INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE] ,spécification de propriétés ,[INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] ,[INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation ,[SHS.INFO] Humanities and Social Sciences/Library and information sciences ,property specification ,modèles de contextes ,Méthodes formelles ,use cases ,ingénierie des exigences ,[INFO.INFO-MO] Computer Science [cs]/Modeling and Simulation ,requirements engineering - Abstract
During the last six years, our research interest has been about how to leverage the integration of formal verification techniques within the industrial software development processes using model driven engineering. We have proposed and evaluated a context description language (called CDL) to ease properties and contexts formalizations while limiting state explosion occurrences. Results of this evaluation were promising (Dhaussy et al., 2009). However, using CDL within industrial settings remains limited due to the lake of methodology and the semantic gap between CDL and models manipulated in industry. In this paper, we propose a solution to face these limits through user oriented models that fill this gap, Au cours de ces six dernières années, nous nous sommes intéressés à la problématique d'intégration des techniques de vérification formelles de type model checking aux processus de développement industriel en tirant profit de l'Ingénierie Dirigée par les Modèles. Nous avons proposé et évalué un langage (nommé CDL) permettant de formaliser les propriétés ainsi que le comportement de l'environnement du modèle à valider pour faciliter la manipulation des outils de vérification formels et limiter le problème de l'explosion combinatoire. Les résultats ont été prometteurs (Dhaussy et al., 2009), mais la manipulation de CDL dans un cadre industriel souffre du manque du cadre méthodologique et constitue une rupture sémantique avec les modèles manipulés, jusqu'alors, dans les processus industriels. Dans cet article, nous proposons une solution à ce problème à travers la définition de modèles, orientés utilisateurs, permettant de faire cette jonction.
- Published
- 2011
23. Distributed System Design with Message Sequence Charts
- Author
-
Krüger, Ingolf Heiko, Broy, Manfred (Prof. Dr.), Broy, Manfred (Prof. Dr. Dr. h.c.), and Wirsing, Martin (Prof. Dr.)
- Subjects
Message Sequence Charts ,MSCs ,Semantics ,Refinement ,Property Specification ,Synthesis of Automata ,Methodology ,Systems Engineering ,Requirements Engineering ,Formal Methods ,ddc:000 ,Allgemeines, Wissenschaft ,Sequenzdiagramme ,Semantik ,Verfeinerung ,Eigenschaftsspezifikation ,Synthese von Automaten ,Methodik ,Formale Methoden - Abstract
The methodical mastery of interaction scenarios is a key factor for capturing and modeling system requirements of distributed, reactive systems. Message Sequence Charts (MSCs) and variants thereof are well-accepted as a graphical description technique for interaction scenarios. MSCs emphasize the inter-component coordination aspect of typically partial system executions; this complements the usually complete behavior description for individual components, as given by state-oriented automaton specifications. The topic of this thesis is the seamless, methodically founded integration of MSCs into the development process for distributed, reactive systems. The comparison of several MSC dialects and automaton models is followed by the definition and analysis of the formal syntax and semantics for the MSC notation used in this thesis. The stream-based system model, underlying the semantics definition, enables the integrated consideration of interaction-oriented and state-oriented system specifications; it also serves as the basis for the introduction of effective refinement notions for MSCs. Next, different MSC interpretations -- in the range from scenario specification to complete behavior descriptions to the specification of unwanted behavior -- are formally defined. In addition, the application of MSCs for the description of safety and liveness properties is analyzed. Finally, two transformation procedures, supporting the transition from interaction scenarios to complete behavior specifications for individual components, are presented. The first one schematically extracts relational assumption/commitment specifications from MSCs. The second one turns MSCs syntactically into corresponding state automata. On the one hand this makes the component properties defined by MSCs accessible to formal analysis; on the other hand this constructively bridges the gap between interaction requirements and component implementations. Die methodische Beherrschung von Interaktionsszenarien ist ein Schlüsselfaktor bei der Erfassung und Modellierung von Systemanforderungen für verteilte, reaktive Systeme. Message Sequence Charts (MSCs) und Varianten davon haben sich als grafische Beschreibungstechnik für Interaktionsszenarien etabliert. MSCs betonen den komponentenübergreifenden Koordinationsaspekt eines typischerweise partiellen Systemablaufs; dies ergänzt die komponentenlokale, jedoch meist vollständige Verhaltensbeschreibung, wie sie durch zustandsorientierte Automatenspezifikationen gegeben ist. Gegenstand der vorliegenden Arbeit ist die durchgängige, methodisch fundierte Integration von MSCs in den Entwicklungsprozeß für verteilte, reaktive Systeme. Nach einer vergleichenden Betrachtung verschiedener MSC-Dialekte und Automatenmodelle wird die formale Syntax und Semantik der in dieser Arbeit verwendeten MSC-Notation definiert und analysiert. Das der Semantikdefinition zugrundeliegende, strombasierte Systemmodell ermöglicht die integrierte Betrachtung interaktions- und zustandsorientierter Systemspezifikationen und dient als Basis für die Einführung effektiver Verfeinerungsbegriffe für MSCs. Im Anschluß daran werden unterschiedliche MSC-Interpretationen -- von der Szenarienspezifikation über die vollständige Verhaltensbeschreibung, bis hin zur Spezifikation von Fehlverhalten -- formal definiert. Zusätzlich wird die Anwendung von MSCs zur Beschreibung von Sicherheits- und Lebendigkeitseigenschaften untersucht. Um den Übergang von Interaktionsszenarien zu vollständigen Verhaltensspezifikationen für einzelne Komponenten methodisch zu unterstützen, werden schließlich zwei Transformationsverfahren angegeben. Das erste extrahiert relationale Assumption/Commitment-Spezifikationen auf schematische Weise aus MSCs. Das zweite wandelt MSCs syntaktisch in korrespondierende Zustandsautomaten um. Dadurch werden einerseits die durch ein MSC definierten Komponenteneigenschaften einer formalen Analyse zugänglich, andererseits wird die Lücke zwischen Interaktionsanforderungen und Komponentenimplementierungen konstruktiv überbrückt.
- Published
- 2007
24. Towards Model Checking OCL
- Subjects
Formal verification ,Object Constraint Language (OCL) ,Temporal Logic ,IR-61727 ,EWI-10041 ,object-based system ,property specification - Abstract
This paper presents a logic, called BOTL (Object-Based Temporal Logic), that facilitates the specification of dynamic and static properties of object-based systems. The logic is based on the branching temporal logic CTL and the Object Constraint Language (OCL). Eventually, the aim is to do model checking. The formal semantics of BOTL is defined in terms of a general operational model that is aimed to be applicable to a wide range of object-oriented languages. A mapping of a large fragment of OCL onto BOTL is defined, thus providing a formal semantics to OCL and, at the same time, permitting model checking of OCL constraints.
- Published
- 2000
25. Towards model checking OCL
- Author
-
Distefano, D.S., Katoen, Joost P., and Rensink, Arend
- Subjects
Formal verification ,Object Constraint Language (OCL) ,Temporal Logic ,IR-61727 ,METIS-119634 ,EWI-10041 ,object-based system ,property specification - Abstract
This paper presents a logic, called BOTL (Object-Based Temporal Logic), that facilitates the specification of dynamic and static properties of object-based systems. The logic is based on the branching temporal logic CTL and the Object Constraint Language (OCL). Eventually, the aim is to do model checking. The formal semantics of BOTL is defined in terms of a general operational model that is aimed to be applicable to a wide range of object-oriented languages. A mapping of a large fragment of OCL onto BOTL is defined, thus providing a formal semantics to OCL and, at the same time, permitting model checking of OCL constraints.
- Published
- 2000
Catalog
Discovery Service for Jio Institute Digital Library
For full access to our library's resources, please sign in.