Search

Your search keyword '"Nickovic, Dejan"' showing total 7 results
Start Over Author "Nickovic, Dejan" Publisher hal ccsd
7 results on '"Nickovic, Dejan"'

1. The 2020 Expert Survey on Formal Methods

Author

Garavel, Hubert, Ter Beek, Maurice H., Van De Pol, Jaco, ter Beek, Maurice H., Nickovic, Dejan, Construction of verified concurrent systems (CONVECS ), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), Istituto di Scienza e Tecnologie dell'Informazione 'A. Faedo' (ISTI), Consiglio Nazionale delle Ricerche [Roma] (CNR), Aarhus University [Aarhus], University of Twente [Netherlands], CNR Istituto di Scienza e Tecnologie dell’Informazione 'A. Faedo' [Pisa] (CNR | ISTI), National Research Council of Italy | Consiglio Nazionale delle Ricerche (CNR), University of Twente, Formal Methods and Tools, ter Beek, Maurice H., and Nickovic, Dejan

Subjects
050101 languages & linguistics, Cybersecurity, Computer science, Software tool, Formal method, 02 engineering and technology, Modelling, Education, 0202 electrical engineering, electronic engineering, information engineering, 0501 psychology and cognitive sciences, [INFO]Computer Science [cs], Survey, Turing, computer.programming_language, Technology transfer, Software engineering, 05 social sciences, Verification, Formal methods, Data science, n/a OA procedure, Key (cryptography), Position (finance), 020201 artificial intelligence & image processing, Safety, computer, Specification
Abstract

International audience; Organised to celebrate the 25th anniversary of the FMICS international conference, the present survey addresses 30 questions on the past, present, and future of formal methods in research, industry, and education. Not less than 130 high-profile experts in formal methods (among whom three Turing award winners and many recipients of other prizes and distinctions) accepted to participate in this survey. We analyse their answers and comments, and present a collection of 111 position statements provided by these experts. The survey is both an exercise in collective thinking and a family picture of key actors in formal methods.

Published
2020
Full Text
View/download PDF

2. The First-Order Logic of Signals

Author

Bakhirkin, Alexey, Ferrère, Thomas, Henzinger, Thomas, Nickovic, Dejan, VERIMAG (VERIMAG - IMAG), 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]), Institute of Science and Technology [Austria] (IST Austria), and Austrian Institute of Technology [Vienna] (AIT)

Subjects
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over time and value parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the microelectronics domain.

Published
2018

3. Second International Competition on Runtime Verification

Author

Falcone, Yliès, Nickovic, Dejan, Reger, Giles, Thoma, Daniel, Compiler Optimization and Run-time Systems (CORSE), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Austrian Institute of Technology [Vienna] (AIT), University of Manchester [Manchester], and Universität zu Lübeck [Lübeck]

Subjects
[INFO.INFO-ES]Computer Science [cs]/Embedded Systems, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]
Abstract

International audience; We report on the Second International Competition on Run-time Verification (CRV-2015). The competition was held as a satellite event of the 15th International Conference on Runtime Verification (RV'15). The competition consisted of three tracks: o✏ine monitoring, online monitoring of C programs, and online monitoring of Java programs. This report describes the format of the competition, the participating teams and submitted benchmarks. We give an example illustrating the two main inputs expected from the participating teams, namely a benchmark (i.e., a program and a property on this program) and a monitor for this benchmark. We also propose some reflection based on the lessons learned.

Published
2015
Full Text
View/download PDF

4. Contracts for Systems Design: Theory

Author

Benveniste, Albert, Caillaud, Benoît, Nickovic, Dejan, Passerone, Roberto, Raclet, Jean-Baptiste, Reinkemeier, Philipp, Sangiovanni-Vincentelli, Alberto, Damm, Werner, Henzinger, Tom, Larsen, Kim Guldstrand, Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques (HYCOMES), 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), Austrian Institute of Technology [Vienna] (AIT), Department of Information Engineering and Computer Science (DISI), University of Trento [Trento], Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), Institute for Information Technology [Oldenburg] (OFFIS), Department of Electrical Engineering and Computer Science [Berkeley] (EECS), University of California [Berkeley] (UC Berkeley), University of California (UC)-University of California (UC), Department für Informatik [Oldenburg], Carl Von Ossietzky Universität Oldenburg = Carl von Ossietzky University of Oldenburg (OFFIS), Institute of Science and Technology [Klosterneuburg, Austria] (IST Austria), Center for Indlejrede Software Systemer (CISS), Aalborg University [Denmark] (AAU), This work was funded in part by the European STREP-COMBEST project number 215543, the Europeanprojects CESAR of the ARTEMIS Joint Undertaking and the European IP DANSE, the Artist DesignNetwork of Excellence number 214373, the TerraSwarm project funded by the STARnet phase of the FocusCenter Research Program (FCRP) administered by the Semiconductor Research Corporation (SRC), theiCyPhy program sponsored by IBM and United Technology Corporation, the VKR Center of ExcellenceMT-LAB, and the German Innovation Alliance on Embedded Systems SPES2020., Inria Rennes Bretagne Atlantique, INRIA, 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), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-É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), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, University of California [Berkeley], University of California-University of California, Carl Von Ossietzky Universität Oldenburg, and Institute of Science and Technology [Austria] (IST Austria)

Subjects
system design, component based design, interface, ContBasedDesign, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, contract, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation
Abstract

Aircrafts, trains, cars, plants, distributed telecommunication military or health care systems,and more, involve systems design as a critical step. Complexity has caused system design times and coststo go severely over budget so as to threaten the health of entire industrial sectors. Heuristic methods andstandard practices do not seem to scale with complexity so that novel design methods and tools based on astrong theoretical foundation are sorely needed. Model-based design as well as other methodologies suchas layered and compositional design have been used recently but a unified intellectual framework with acomplete design flow supported by formal tools is still lacking.Recently an “orthogonal” approach has been proposed that can be applied to all methodologies introducedthus far to provide a rigorous scaffolding for verification, analysis and abstraction/refinement: contractbaseddesign. Several results have been obtained in this domain but a unified treatment of the topic that canhelp in putting contract-based design in perspective is missing. This paper intends to provide such treatmentwhere contracts are precisely defined and characterized so that they can be used in design methodologiessuch as the ones mentioned above with no ambiguity. In addition, the paper provides an important linkbetween interface and contract theories to show similarities and correspondences.This paper is complemented by a companion paper where contract based design is illustrated throughuse cases.

Published
2015

5. Contracts for Systems Design: Methodology and Application cases

Author

Benveniste, Albert, Caillaud, Benoît, Nickovic, Dejan, Passerone, Roberto, Raclet, Jean-Baptiste, Reinkemeier, Philipp, Sangiovanni-Vincentelli, Alberto, Damm, Werner, Henzinger, Tom, Larsen, Kim Guldstrand, Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques (HYCOMES), 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), 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), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-É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), Austrian Institute of Technology [Vienna] (AIT), Department of Information Engineering and Computer Science (DISI), University of Trento [Trento], Assistance à la Certification d’Applications DIstribuées et Embarquées (IRIT-ACADIE), Institut de recherche en informatique de Toulouse (IRIT), Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées, Institute for Information Technology [Oldenburg] (OFFIS), Department of Electrical Engineering and Computer Science [Berkeley] (EECS), University of California [Berkeley], University of California-University of California, Department für Informatik [Oldenburg], Carl Von Ossietzky Universität Oldenburg, Institute of Science and Technology [Austria] (IST Austria), Center for Indlejrede Software Systemer (CISS), Aalborg University [Denmark] (AAU), This work was funded in part by the European STREP-COMBEST project number 215543, the Europeanprojects CESAR of the ARTEMIS Joint Undertaking and the European IP DANSE, the Artist DesignNetwork of Excellence number 214373, the TerraSwarm project funded by the STARnet phase of the FocusCenter Research Program (FCRP) administered by the Semiconductor Research Corporation (SRC), theiCyPhy program sponsored by IBM and United Technology Corporation, the VKR Center of ExcellenceMT-LAB, and the German Innovation Alliance on Embedded Systems SPES2020., Inria Rennes Bretagne Atlantique, INRIA, 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), Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT)-Toulouse Mind & Brain Institut (TMBI), Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT), University of California [Berkeley] (UC Berkeley), University of California (UC)-University of California (UC), Carl Von Ossietzky Universität Oldenburg = Carl von Ossietzky University of Oldenburg (OFFIS), and Institute of Science and Technology [Klosterneuburg, Austria] (IST Austria)

Subjects
system design, component based design, interface, ContBasedDesign, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, contract, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation
Abstract

Recently, contract based design has been proposed as an ”orthogonal” approach that can beapplied to all methodologies proposed so far to cope with the complexity of system design. Contract baseddesign provides a rigorous scaffolding for verification, analysis and abstraction/refinement. Companionreport RR-8759 proposes a unified treatment of the topic that can help in putting contract-based design in perspective.This paper complements RR-8759 by further discussing methodological aspects of system design withcontracts in perspective and presenting two application cases.The first application case illustrates the use of contracts in requirement engineering, an area of system designwhere formal methods were scarcely considered, yet are stringently needed. We focus in particular to thecritical design step by which sub-contracts are generated for suppliers from a set of different viewpoints(specified as contracts) on the global system. We also discuss important issues regarding certification inrequirement engineering, such as consistency, compatibility, and completeness of requirements.The second example is developed in the context of the Autosar methodology now widely advocated inthe automotive sector. We propose a contract framework to support schedulability analysis, a key step inAutosar methodology. Our aim differs from the many proposals for compositional schedulability analysisin that we aim at defining sub-contracts for suppliers, not just performing the analysis by parts—we knowfrom companion paper RR-8759 that sub-contracting to suppliers differs from a compositional analysis entirelyperformed by the OEM. We observe that the methodology advocated by Autosar is in contradiction withcontract based design in that some recommended design steps cannot be refinements. We show how tocircumvent this difficulty by precisely bounding the risk at system integration phase. Another feature ofthis application case is the combination of manual reasoning for local properties and use of the formalcontract algebra to lift a collection of local checks to a system wide analysis.

Published
2015

6. Compositional Contract Abstraction for System Design

Author

Benveniste, Albert, Nickovic, Dejan, Henzinger, Thomas, Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques (HYCOMES), 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), 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), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-É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), AIT, Austrian Institute of Technology [Vienna] (AIT), Institute of Science and Technology [Austria] (IST Austria), INRIA, 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), and Institute of Science and Technology [Klosterneuburg, Austria] (IST Austria)

Subjects
system design, component based design, interface, ContBasedDesign, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, abstract interpretation, abstraction, contract
Abstract

Contract-based design has been recently proposed as a framework for concurrent system design in the context of complex supplier chains, where sub-system design can be sub-contracted to suppliers while guaranteeing correct system integration. A unifying meta-theory of contracts was proposed in [Benveniste et al. 2012], which subsumes known frameworks such as interface theories, modal interfaces, and Assume/Guarantee contracts. This report proposes, for this meta-theory of contracts, a generic abstraction technique allowing to prove contract properties based on their abstractions. More precisely, we show how to lift abstractions, from components to contracts, in a systematic way. In doing so, fundamental relations such as being a correct implementation or a valid environment, refining, can be checked on abstractions. Our abstraction technique is fully compositional with respect to contract conjunction. Compositionality of abstraction with respect to contract composition is only partially achieved. We believe that the results we obtain are the best achievable ones and we explain the obstructions we see against improving them. Our abstraction technique complements observers, proposed as a testing technique adapted to contracts in [6]. The latter allow disproving properties, whereas abstraction allows proving them. Key-words: system design, component based design, contract, interface, abstraction, abstract interpretation.; La conception par contrats a été proposée récemment comme une approche formelle pour la conception de systèmes permettant le développement parallèle de sysèmes dans un contexte de chaine complexe de sous-traitants. Les théories d'interfaces, les interfaces modales et les contrats hypothèse/garantie, sont autant de formalismes en ce sens. L'article collectif [Benveniste et al. 2012] a proposé une "méta-théorie" des contrats, unifiant les formalismes précédents. Le présent rapport développe, pour cette méta-théorie des contrats, une technique systématique d'abstraction. Les propriétés fondamentales des contrats (relation d'implémentation, d'environnement, de raffinement) peuvent être prouvées sur les abstractions. L'abstraction proposée offre de bonnes propriétés de compositionnalité, même si toutes les propriétés souhaitables ne sont pas valides. Cette technique d'abstraction complète celle des observateurs, qui permettent d'invalider des propriétés de contrats par une approche de type test. Mots-clés : conception des systèmes, composant, contrat, interface, abstraction, interprétation abstraite.

Published
2014

7. Vérification de propriétés temporisées et hybrides: théorie et applications

Author

Nickovic, Dejan, Nickovic, Dejan, VERIMAG (VERIMAG - IMAG), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Grenoble (INPG)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Université Joseph Fourier - Grenoble 1 (UJF), Université Joseph-Fourier - Grenoble I, and Maler Oded

Subjects
temporal testers, [INFO.INFO-OH] Computer Science [cs]/Other [cs.OH], monitoring, property, temporal logic, synthesis, timed automata, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], analog and mixed-signal
Abstract

The growth of consumer embedded devices, where digital, analog and software components are often combined together on a single chip, results in an increase of complexity of the design and verification processes. The validation of such analog and mixed-signal systems largely relies on simulation-based techniques combined with often ad-hoc analysis methods. This thesis is motivated by the export of property-based formal techniques to the validation of analog and mixed-signal systems, at their continuous and timed levels of abstraction. Since the formal verification of non-trivial continuous systems remains very difficult, we resort to a lighter validation technique, that is, property-based monitoring.We define signal temporal logic STL as a high-level specification language that allows expressing temporal properties of continuous and timed signals. STL is as an extension of the realtime metric interval temporal logic MITL, where continuous signals are transformed into Boolean ones using numerical predicates, and the temporal relations between them are expressed using standard real-time temporal operators whose atomic propositions correspond to those predicates.We develop two monitoring procedures, offline and incremental, for checking the correctness of simulation traces with respect to STL properties and implement them into a stand alone analog monitoring tool (AMT). The property-based monitoring framework is applied, using the AMT tool, to two real-world case studies, considering properties of a FLASH memory cell and a DDR2 memory interface. We also consider the problem of property-based formal verification of timed systems, and develop a modular translation from MITL formulae with past and future operators to timed automata. The construction that we propose is based on temporal testers, a special class of input/output timed automata that realize the sequential functions defined by the semantics of MITL operators. We first show how every MITL formula can be expressed using six basic temporal operators (three for past and three for future) and show how to build a temporal tester for each of these operators. Temporal testers for arbitrary MITL formulae are obtained by composing these elementary testers. Finally, we develop a procedure for automatic synthesis of controllers from high-level specifications expressed in the bounded fragment of metric temporal logic (MTL). We propose a translation from properties specified in this real-time logic and under bounded variability assumption, into deterministic timed automata to which we apply safety synthesis algorithms to build a controller that satisfies the specification by construction., Le développement croissant de systèmes embarqués de consommation, où les composants numériques, analogiques et logiciels sont combinés sur une même puce, résulte en une augmentation de la complexité des processus de conception et de vérification. La validation de tels systèmes analogiques et à signaux-mixtes reste largement basée sur des techniques de simulation, qui sont souvent combinées avec des méthodes d'analyse de nature ad-hoc. Cette thèse est motivée par l'exportation de méthodes formelles basées sur des propriétés, vers leur application à la validation de systèmes analogiques et à signaux mixtes, considérés à leur niveaux d'abstraction continu et temporisé.Etant-donné que la vérification formelle de systèmes continus non-triviaux reste très difficile, nous nous tournons vers une méthode de validation plus légère appelée le monitoring basé sur des propriétés. Nous définissons signal temporal logic STL comme langage de spécification de haut niveau qui permet d'exprimer des propriétés temporelles de signaux continus et temporisés. STL est une extension de la logique de temps-réel metric interval temporal logic MITL, où les signaux continus sont transformés en signaux Booléens avec des prédicats numériques, et les relations temporelles entre ces signaux son exprimées avec les opérateurs temporels habituels dont les propositions atomiques correspondent à ces prédicats. Nous développons deux procédures de monitoring, une offline et une incrémantale, qui permettent de vérifier si les traces de simulations sont correctes par rapport aux propriétés STL. Les deux procédures sont implantées en outil de monitoring analogique AMT. Notre approche de monitoring basé sur des propriétés est appliquée, en utilisant AMT, à deux études de cas réalistes, où nous étudions des propriétés d'une mémoire de type FLASH et d'une interface de mémoire DDR2. Nous considérons aussi le problème de vérification formelle de systèmes temporisés, et développons une traduction modulaire des formules MITL avec les opérateurs futurs et passés, vers des automates temporisés. La construction que nous proposons est basée sur les testeurs temporels, une classe spécifique d'automates avec les entrées et les sorties qui réalisent la fonction séquentielle définie par la sémantique des opérateurs MITL. Nous montrons d'abord comment chaque formule MITL peut être exprimée avec six opérateurs basiques (trois opérateurs passés et trois futurs) et nous proposons une construction de testeurs temporels à partir de ces opérateurs. Les testeurs temporels pour des formules MITL arbitraires sont obtenus en composant ces testeurs élémentaires.Finalement, nous développons une procédure pour la synthèse automatique de contrôleurs à partir des spécifications de haut niveau exprimées avec le fragment borné de metric temporal logic (MTL). Nous proposons une traduction des propriétés spécifiées dans cette logique temporisée vers des automates temporisés déterministes, en supposant la variabilité bornée. Ensuite, nous pouvons appliquer à ces automates les algorithmes habituels de synthèse de sûreté pour construire un contrôleur qui satisfait la spécification par construction.

Published
2008

Catalog

Books, media, physical & digital resources
See catalog results