| 1. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
A Unified Approach for Static and Runtime Verification: Framework and Applications
- 2012
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642340253 ; 7609 LNCS:PART 1, s. 312-326
-
Konferensbidrag (refereegranskat)abstract
- Static verification of software is becoming ever more effective and efficient. Still, static techniques either have high precision, in which case powerful judgements are hard to achieve automatically, or they use abstractions supporting increased automation, but possibly losing important aspects of the concrete system in the process. Runtime verification has complementary strengths and weaknesses. It combines full precision of the model (including the real deployment environment) with full automation, but cannot judge future and alternative runs. Another drawback of runtime verification can be the computational overhead of monitoring the running system which, although typically not very high, can still be prohibitive in certain settings. In this paper, we propose a framework to combine static analysis techniques and runtime verification with the aim of getting the best of both techniques. In particular, we discuss an instantiation of our framework for the deductive theorem prover KeY, and the runtime verification tool LARVA. Apart from combining static and dynamic verification, this approach also combines the data centric analysis of KeY with the control centric analysis of LARVA. An advantage of the approach is that, through the use of a single specification which can be used by both analysis techniques, expensive parts of the analysis could be moved to the static phase, allowing the runtime monitor to make significant assumptions, dropping parts of expensive checks at runtime. We also discuss specific applications of our approach.
|
|
| 2. |
- Angelov, Krasimir, 1978, et al.
(författare)
-
A Framework for Conflict Analysis of Normative Texts Written in Controlled Natural Language
- 2013
-
Ingår i: Journal of Logic and Algebraic Programming. - : Elsevier BV. - 1567-8326. ; 82:5-7, s. 216-240
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper we are concerned with the analysis of normative conflicts, or the detection of conflicting obligations, permissions and prohibitions in normative texts written in a Controlled Natural Language (CNL). For this we present AnaCon, a proof-of-concept system where normative texts written in CNL are automatically translated into the formal language CL using the Grammatical Framework (GF). Such CL expressions are then analysed for normative conflicts by the CLAN tool, which gives counter-examples in cases where conflicts are found. The framework also uses GF to give a CNL version of the counter-example, helping the user to identify the conflicts in the original text. We detail the application of AnaCon to two case studies and discuss the effectiveness of our approach.
|
|
| 3. |
- Asarin, E., et al.
(författare)
-
Low dimensional hybrid systems - decidable, undecidable, don't know
- 2012
-
Ingår i: Information and Computation. - : Elsevier BV. - 0890-5401. ; 211, s. 138-159
-
Tidskriftsartikel (refereegranskat)abstract
- Even though many attempts have been made to define the boundary between decidable and undecidable hybrid systems, the affair is far from being resolved. More and more low dimensional systems are being shown to be undecidable with respect to reachability, and many open problems in between are being discovered. In this paper, we present various two-dimensional hybrid systems for which the reachability problem is undecidable. We show their undecidability by simulating Minsky machines. Their proximity to the decidability frontier is understood by inspecting the most parsimonious constraints necessary to make reachability over these automata decidable. We also show that for other two-dimensional systems, the reachability question remains unanswered, by proving that it is as hard as the reachability problem for piecewise affine maps on the real line, which is a well known open problem.
|
|
| 4. |
|
|
| 5. |
- Camilleri, John J., 1986, et al.
(författare)
-
A CNL for Contract-Oriented Diagrams
- 2014
-
Ingår i: Lecture notes in computer science: Proceedings of the 4th International Workshop on Controlled Natural Language, CNL 2014, Galway, Ireland, August 20-22, 2014. - Cham : Springer International Publishing. - 0302-9743 .- 1611-3349. - 9783319102238 ; 8625, s. 135-146
-
Konferensbidrag (refereegranskat)abstract
- We present a first step towards a framework for defining and manipulating normative documents or contracts described as Contract-Oriented (C-O) Diagrams. These diagrams provide a visual representation for such texts, giving the possibility to express a signatory's obligations, permissions and prohibitions, with or without timing constraints, as well as the penalties resulting from the non-fulfilment of a contract. This work presents a CNL for verbalising C-O Diagrams, a web-based tool allowing editing in this CNL, and another for visualising and manipulating the diagrams interactively. We then show how these proof-of-concept tools can be used by applying them to a small example.
|
|
| 6. |
- Díaz, Gregorio, et al.
(författare)
-
Specification and Verification of Normative Texts using C-O Diagrams
- 2014
-
Ingår i: IEEE Transactions on Software Engineering. - 0098-5589. ; 40:8, s. 795-817
-
Tidskriftsartikel (refereegranskat)abstract
- C-O diagrams have been introduced as a means to have a more visual representation of normative texts and electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as the penalties resulting from non-fulfillment of their obligations and prohibitions. In such diagrams we are also able to represent absolute and relative timing constraints. In this paper we present a formal semantics for C-O diagrams based on timed automata extended with information regarding the satisfaction and violation of clauses in order to represent different deontic modalities. As a proof of concept, we apply our approach to two different case studies, where the method presented here has successfully identified problems in the specification.
|
|
| 7. |
|
|
| 8. |
- Hansen, H. A., et al.
(författare)
-
Reachability analysis of complex planar hybrid systems
- 2013
-
Ingår i: Science of Computer Programming. - : Elsevier BV. - 0167-6423. ; 78:12, s. 2511-2536
-
Tidskriftsartikel (refereegranskat)abstract
- Hybrid systems are systems that exhibit both discrete and continuous behavior. Reachability, the question of whether a system in one state can reach some other state, is undecidable for hybrid systems in general. In this paper we are concerned with GSPDIs, 2-dimensional systems generalizing SPDIs (planar hybrid systems based on "simple polygonal differential inclusions"), for which reachability have been shown to be decidable. GSPDIs are useful to approximate 2-dimensional control systems, allowing the verification of safety properties of such systems. In this paper we present the following two contributions: (i) an optimized algorithm that answers reachability questions for GSPDIs, where all cycles in the reachability graph are accelerated. (ii) An algorithm by which more complex planar hybrid automata are over-approximated by GSPDIs subject to two measures of precision. We prove soundness, completeness, and termination of both algorithms, and discuss their implementation. (C) 2013 Elsevier B.V. All rights reserved.
|
|
| 9. |
- Hansen, Hallstein A., et al.
(författare)
-
Reachability Analysis of GSPDIs: Theory, Optimization, and Implementation
- 2010
-
Ingår i: 25th Annual ACM Symposium on Applied Computing -Software Verification and Testing track (SAC-SVT'10). - 9781605586397
-
Konferensbidrag (refereegranskat)abstract
- Analysis of systems containing both discrete and continuous dynamics, hybrid systems, is a difficult issue. Most problems have been shown to be undecidable, with the exception of a few classes where the dynamics are restricted and/or the dimension is low. In this paper we present some theoretical results concerning the decidability of the reachability problem for a class of planar hybrid systems called Generalized Polygonal Hybrid Systems (GSPDI). These new results provide means to optimize a previous reachability algorithm, making the implementation feasible. We also discuss the implementation of the algorithm into a tool.
|
|
| 10. |
- Hansen, Hallstein Asheim, et al.
(författare)
-
Reachability analysis of non-linear planar autonomous systems
- 2012
-
Ingår i: Lecture Notes in Computer Science (LNCS). - 0302-9743. ; 7141, s. 206-220
-
Konferensbidrag (refereegranskat)abstract
- Many complex continuous systems are modeled as non-linear autonomous systems, i.e., by a set of differential equations with one independent variable. Exact reachability, i.e., whether a given configuration can be reached by starting from an initial configuration of the system, is undecidable in general, as one needs to know the solution of the system of equations under consideration. In this paper we address the reachability problem of planar autonomous systems approximatively. We use an approximation technique which "hybridizes" the state space in the following way: the original system is partitioned into a finite set of polygonal regions where the dynamics on each region is approximated by constant differential inclusions. Besides proving soundness, completeness, and termination of our algorithm, we present an implementation, and its application into (classical) examples taken from the literature.
|
|
