Coverage-Based Testing with Symbolic Transition Systems

AbstractAIGEN is an open source tool for the generation of transition systems in a symbolic representation. To ensure diversity, it employs a uniform random sampling over the space of all Boolean functions with a given number of variables. AIGEN relies on reduced ordered binary decision diagrams (ROBDDs) and canonical disjunctive normal form (CDNF) as canonical representations that allow us to enumerate Boolean functions, in the former case with an encoding that is inspired by data structures used to implement ROBDDs. Several parameters allow the user to restrict generation to Boolean functions or transition systems with certain properties, which are then output in AIGER format. We report on the use of AIGEN to generate random benchmark problems for the reactive synthesis competition SYNTCOMP 2019, and present a comparison of the two encodings with respect to time and memory efficiency in practice.

Download Full-text

Model-Based Testing from Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts

Testing Software and Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-319-25945-1_3 ◽

2015 ◽

pp. 35-51 ◽

Cited By ~ 2

Author(s):

Imen Boudhiba ◽

Christophe Gaston ◽

Pascale Le Gall ◽

Virgile Prevosto

Keyword(s):

Input Output ◽

Transition Systems ◽

Model Based ◽

Model Based Testing ◽

Symbolic Transition Systems

Download Full-text

Natural Projection as Partial Model Checking

Journal of Automated Reasoning ◽

10.1007/s10817-020-09568-7 ◽

2020 ◽

Vol 64 (7) ◽

pp. 1445-1481

Author(s):

Gabriele Costa ◽

Letterio Galletta ◽

Pierpaolo Degano ◽

David Basin ◽

Chiara Bodei

Keyword(s):

Model Checking ◽

Control Theory ◽

Control Flow ◽

Point Of View ◽

Natural Projection ◽

Transition Systems ◽

Partial Model ◽

Finite State ◽

Symbolic Transition Systems ◽

Large Systems

Abstract Verifying the correctness of a system as a whole requires establishing that it satisfies a global specification. When it does not, it would be helpful to determine which modules are incorrect. As a consequence, specification decomposition is a relevant problem from both a theoretical and practical point of view. Until now, specification decomposition has been independently addressed by the control theory and verification communities through natural projection and partial model checking, respectively. We prove that natural projection reduces to partial model checking and, when cast in a common setting, the two are equivalent. Apart from their foundational interest, our results build a bridge whereby the control theory community can reuse algorithms and results developed by the verification community. Furthermore, we extend the notions of natural projection and partial model checking from finite-state to symbolic transition systems and we show that the equivalence still holds. Symbolic transition systems are more expressive than traditional finite-state transition systems, as they can model large systems, whose behavior depends on the data handled, and not only on the control flow. Finally, we present an algorithm for the partial model checking of both kinds of systems that can be used as an alternative to natural projection.

Download Full-text

Symbolic-Based Monitoring for Embedded Applications

Human-Computer Interaction ◽

10.4018/978-1-4666-8789-9.ch043 ◽

2015 ◽

pp. 939-961

Author(s):

Pramila Mouttappa ◽

Stephane Maag ◽

Ana Cavalli

Keyword(s):

System Design ◽

Research Community ◽

Input Output ◽

Transition Systems ◽

Execution Traces ◽

Novel Approach ◽

Security Properties ◽

Symbolic Transition Systems ◽

And Control ◽

Embedded Applications

Testing embedded systems to find errors and to validate that the implemented system as per the specifications and requirements has become an important part of the system design. The research community has proposed several formal approaches these last years, but most of them only consider the control portion of the protocol, neglecting the data portions, or are confronted with an overloaded amount of data values to consider. In this chapter, the authors present a novel approach to model protocol properties of embedded application in terms of Input-Output Symbolic Transition Systems (IOSTS) and show how they can be tested on real execution traces taking into account the data and control portions. These properties can be designed to test the conformance of a protocol as well as security aspects. A parametric trace slicing approach is presented to match trace and property. This chapter is illustrated by an application to a set of real execution traces extracted from a real automotive Bluetooth framework with functional and security properties.

Download Full-text