| 34961. |
|
|
| 34962. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
A circuit approach to LTL model checking
- 2013
-
Ingår i: 13th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2013; Portland, OR; United States; 20 October 2013 through 23 October 2013. - 9780983567837 ; , s. 53-60
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a method for translating formulas written in assertion languages such as LTL into a monitor circuit suitable for model checking. Unlike the conventional approach, no automata is generated for the property, but instead the monitor is built directly from the property formula through a recursive traversal. This method was first introduced by Pnueli et. al. under the name of Temporal Testers. In this paper, we show the practicality of temporal testers through experimental evaluation, as well as offer a self-contained exposition for how to construct them in manner that meets the requirements of industrial model checking tools. These tools tend to operate on logic circuits with sequential elements, rather than transition relations, which means we only need to consider so called positive testers with no future references. This restriction both simplifies the presentation and allows for more efficient monitors to be generated. In the final part of the paper, we suggest several possible optimizations that can improve the quality of the monitors, and conclude with experimental data.
|
|
| 34963. |
- Lindström Claessen, Koen, 1975
(författare)
-
A Coverage Analysis for Safety Property Lists
- 2007
-
Ingår i: Conference on Formal Methods for Computer Aided Design (FMCAD), Austin, TX, NOV 11-14, 2007. - 9780769530239 ; , s. 139-145
-
Konferensbidrag (refereegranskat)abstract
- We present a coverage analysis that can be used inproperty-based verification. The analysis helps identifying ”forgottencases”; scenarios where the property list under analysisdoes not constrain a certain output at a certain point in time.These scenarios can then be manually investigated, possibly leadingto new, previously forgotten properties being added. As thereoften exist cases in which outputs are not supposed to be specified,we also provide means for the specificier to annotate properties inorder to control what cases are supposed to be underconstrained.Two main differences with earlier proposed similar analysesexist: The presented analysis is design-independent, and it makesan explicit distinction between intentionally and unintentionallyunderspecified behavior.
|
|
| 34964. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
A FAITHFUL SEMANTICS FOR GENERALISED SYMBOLIC TRAJECTORY EVALUATION
- 2009
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 5:2, s. 1 (artno)-
-
Tidskriftsartikel (refereegranskat)abstract
- Generalised Symbolic Trajectory Evaluation (GSTE) is a high-capacity formal verification technique for hardware. GSTE is an extension of Symbolic Trajectory Evaluation (STE). The difference is that STE is limited to properties ranging over finite time-intervals whereas GSTE can deal with properties over unbounded time. GSTE uses abstraction, meaning that details of the circuit behaviour are removed from the circuit model. This improves the capacity of the method, but has as down-side that certain properties cannot be proven if the wrong abstraction is chosen. A semantics for GSTE can be used to predict and understand why certain circuit properties can or cannot be proven by GSTE. Several semantics have been described for GSTE by Yang and Seger. These semantics, however, are not faithful to the proving power of GSTE-algorithms, that is, the GSTE-algorithms are incomplete with respect to the semantics. The reason is that these semantics do not capture the abstraction used in GSTE precisely. The abstraction used in GSTE makes it hard to understand why a specific property can, or cannot, be proven by GSTE. The semantics mentioned above cannot help the user in doing so. So, in the current situation, users of GSTE often have to revert to the GSTE algorithm to understand why a property can or cannot be proven by GSTE. The contribution of this paper is a faithful semantics for GSTE. That is, we give a simple formal theory that deems a property to be true if-and-only-if the property can be proven by a GSTE-model checker. We prove that the GSTE algorithm is sound and complete with respect to this semantics. Furthermore, we show that our semantics for GSTE is a generalisation of the semantics for STE and give a number of additional properties relating the two semantics.
|
|
| 34965. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
A liveness checking algorithm that counts
- 2012
-
Ingår i: 2012 Formal Methods in Computer-Aided Design, FMCAD 2012. - 9781467348324 ; , s. 52-59
-
Konferensbidrag (refereegranskat)abstract
- We present a simple but novel algorithm for checking liveness properties of finite-state systems, called k-Liveness, which is based on counting and bounding the number of times a fairness constraint can become true. Our implementation of the algorithm is completely SAT-based, works fairly well in practice, and is competitive in performance with alternative methods. In addition, we present a pre-processing technique which can automatically derive extra fairness constraints for any given liveness problem. These constraints can be used to potentially boost the performace of any liveness algorithm. The experimental results show that the extra constraints are particularly beneficial in combination with our k-Liveness algorithm.
|
|
| 34966. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
A Semantics for Distributed Erlang
- 2005
-
Ingår i: Proceedings of the ACM SIGPLAN 2005 Erlang Workshop. - 1595930663
-
Konferensbidrag (refereegranskat)abstract
- We propose an extension to Fredlund's formal semantics for Erlang thatmodels the concept of nodes. The motivation is that there existsequences of events that can occur in practice, but are impossible todescribe using a single-node semantics, such as Fredlund's. Theconsequence is that some errors in distributed systems might not bedetected by model checkers based on Fredlund's original semantics, orby other single-node verification techniques such as testing. Ourextension is modest; it re-uses most of Fredlund's work but adds anextra layer at the top-level.
|
|
| 34967. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
A supervisory control algorithm based on property-directed reachability
- 2017
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319703886 ; 10629 LNCS, s. 115-130
-
Konferensbidrag (refereegranskat)abstract
- We present an algorithm for synthesising a controller (supervisor) for a discrete event system (DES) based on the property-directed reachability (PDR) model checking algorithm. The discrete event systems framework is useful in both software, automation and manufacturing, as problems from those domains can be modelled as discrete supervisory control problems. As a formal framework, DES is also similar to domains for which the field of formal methods for computer science has developed techniques and tools. In this paper, we attempt to marry the two by adapting PDR to the problem of controller synthesis. The resulting algorithm takes as input a transition system with forbidden states and uncontrollable transitions, and synthesises a safe and minimally-restrictive controller, correct-by-design. We also present an implementation along with experimental results, showing that the algorithm has potential as a part of the solution to the greater effort of formal supervisory controller synthesis and verification.
|
|
| 34968. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
An Operational Semantics for Weak PSL
- 2004
-
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. ; 3312, s. 337-351
-
Tidskriftsartikel (refereegranskat)abstract
- Extending linear temporal logic by adding regular expressions increases its expressiveness. However, as for example, problems in recent versions of Accellera's Property Specification Language (PSL) as well as in OpenVera's ForSpec and other property languages show, it is a non-trivial task to give a formal denotational semantics with desirable properties to the resulting logic. In this paper, we argue that specifying an operational semantics may be helpful in guiding this work, and as a bonus leads to an implementation of the logic for free. We give a concrete operational semantics for Weak PSL, which is the safety property subset of PSL. We also propose a denotational semantics which we show to be equivalent to the operational one. This semantics is inspired by a new denotational semantics proposed in recent related work.
|
|
| 34969. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Automated Inference of Finite Unsatisfiability
- 2011
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 47:2, s. 111-132
-
Tidskriftsartikel (refereegranskat)abstract
- We present Infinox, an automated tool for analyzing first-order logic problems, aimed at showing finite unsatisfiability, i.e., the absence of models with finite domains. Finite satisfiability is not a decidable problem (only semi-decidable), which means that such a tool can never be complete. Nonetheless, our hope is that Infinox be a useful complement to finite model finders in practice. Infinox uses several different proof techniques for showing infinity of a set, each of which requires the identification of a function or a relation with particular properties. Infinox enumerates candidates to such functions and relations, and subsequently uses an automated theorem prover as a sub-procedure to try to prove the resulting proof obligations. We have evaluated Infinox on the relevant problems from the TPTP benchmark suite, and we are able to automatically show finite unsatisfiability for over 25% of these problems.
|
|
| 34970. |
- Lindström Claessen, Koen, 1975, et al.
(författare)
-
Automating Inductive Proofs using Theory Exploration
- 2013
-
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. - 9783642385735 ; 7898, s. 392-406
-
Konferensbidrag (refereegranskat)abstract
- HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.
|
|
