Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
Approximate Active Learning of Nondeterministic Input Output Transition Systems
Full text linkConstructing a model of a system for model-based testing, simulation, or model checking can be cumbersome for existing, third party, or legacy components. Active automata learning, a form of black-box reverse engineering, and in particular Angluin’s L* algorithm, support the automatic inference of a model from a System Under Learning (SUL), through observations and tests. Most of the algorithms based on L* , however, deal with complete learning of deterministic models, thus being unable to cope with nondeterministic SULs, and always learning a complete and correct model as they are based on equivalence between the SUL and the model. We present an adaptation of Angluin’s algorithm for active learning of nondeterministic, input-enabled, input-output transition systems. It enables dealing with nondeterministic SULs, and it allows to construct partial, or approximate models, by expressing the relation between the SUL and the learned model as a refinement relation, not necessarily an equivalence. Thus, we can reason about learned models being more, or less precise than others. Approximate learning has benefits in model-based regression testing: we need not to wait until a complete model has been learned; with an approximate model ioco-based regression testing can start
Preface
Full text linkThe 15th International Workshop on Automated Verification of Critical Systems was hosted by the School of Mathematical and Computer Sciences within Heriot-Watt University on September 2-4, 2015 in Edinburgh, United Kingdom. The 6th AI4FM workshop, which was held on 1 September, was co-located with AVoCS
ThreadSafe: Static Analysis for Java Concurrency
Full text linkThreadSafe is a commercial static analysis tool that focuses on detection of Java concurrency defects. ThreadSafe’s bug-finding capabilities and its look and feel are presented through examples of bugs found in the codebases of two widely-used open source projects
First-order logic for safety verification of hedge rewriting systems
Full text linkIn this paper we deal with verification of safety properties of hedge rewriting systems and their generalizations. The verification problem is translated to a purely logical problem of finding a finite countermodel for a first-order formula, which is further tackled by a generic finite model finding procedure. We show that the proposed approach is at least as powerful as the methods using regular invariants. At the same time the finite countermodel method is shown to be efficient and applicable to the wide range of systems, including the protocols operating on unranked trees
Conditional Lemma Discovery and Recursion Induction in Hipster
Full text linkHipster is a theory exploration tool for the proof assistant Isabelle/HOL. It automatically discovers lemmas about given recursive functions and datatypes and proves them by induction. Previously, only equational properties could be discovered. Conditional lemmas, for example required when reasoning about sorting, has been beyond the scope of theory exploration. In this paper we describe an extension to Hipster to also support discovery and proof of conditional lemmas. We also present a new automated tactic, which uses recursion induction. Recursion induction follows the recursive structure of a function definition through its termina- tion order, as opposed to structural induction, which follows that of the datatype. We find that the addition of recursion induction increases the number of proofs completed automatically, both for conditional and equational statements.
Distributed Verification of Rare Properties using Importance Splitting Observers
Full text linkRare properties remain a challenge for statistical model checking (SMC) due to the quadratic scaling of variance with rarity. We address this with a variance reduction framework based on lightweight importance splitting observers. These expose the model-property automaton to allow the construction of score functions for high performance algorithms. The confidence intervals defined for importance splitting make it appealing for SMC, but optimising its performance in the standard way makes distribution inefficient. We show how it is possible to achieve equivalently good results in less time by distributing simpler algorithms. We first explore the challenges posed by importance splitting and present an algorithm optimised for distribution. We then define a specific bounded time logic that is compiled into memory-efficient observers to monitor executions. Finally, we demonstrate our framework on a number of challenging case studies
Automated Verification of Asynchronous Communicating Systems with TLA+
Full text linkVerifying the compatibility of communicating peers is a crucial issue in critical distributed systems. Unlike the synchronous world, the asynchronous world covers a wide range of message ordering paradigms (e.g. FIFO or causal) that are instrumental to the compatibility of peer compositions. We propose a framework that takes into account the variety of asynchronous communication models and compatibility properties. The notions of peer, communication model, system and compatibility criteria are formalized in TLA+ to benefit from its verification tools. We present an implemented toolchain that generates TLA+ specifications from the behavioral descriptions of peers and checks compatibility of the composition with respect to given communication models and compatibility criteria
On the decidability of model checking LTL fragments in monotonic extensions of Petri nets
Full text linkWe study the model checking problem for monotonic extensions of Petri Nets, namely for two extensions of Petri nets: reset nets (nets in which places can be emptied by the firing of a transition with a reset arc) and ν-Petri nets (nets in which tokens are pure names that can be matched with equality and dynamically created). We consider several fragments of LTL for which the model checking problem is decidable for P/T nets. We first show that for those logics, model checking of reset nets is undecidable. We transfer those results to the case of ν-Petri nets. In order to cope with these negative results, we define a weaker fragment of LTL, in which negation is not allowed. We prove that for that fragment, the model checking of both reset nets and ν-Petri nets is decidable, though with a non primitive recursive complexity. Finally, we prove that the model checking problem for a version of that fragment with universal interpretation is undecidable even for P/T nets
Permissive strategies in timed automata and games
Full text linkTimed automata are a convenient framework for modelling and reasoning about real-time systems. While these models are now well-understood, they do not offer a convenient way of taking timing imprecisions into account. Several solutions (e.g. parametric guard enlargement) have been proposed over the last ten years to take such imprecisions into account. In this paper, we propose a novel approach for handling robust reachability, based on permissive strategies. While classical strategies propose to play an action at an exact point in time, permissive strategies consider intervals of possible dates when to play the selected action. In other words, the controller specifies an interval of time delays for actions to be executed in a more flexible way. With such a permissive strategy, we associate a penalty, which is the inverse of the length of the proposed interval, and accumulates along the run. We show that in that setting, optimal strategies can be computed in polynomial time for one-clock timed automata