ABSTRACT. This paper complements our previous work on formal modelling of resource-bounded context-aware systems, which handle inconsistent context information using defeasible reasoning, by focusing on automated analysis and verification. A case study demonstrates how model checking techniques can be used to formally analyse quantitative and qualitative properties of a context-aware system based on message passing among agents. The behaviour (semantics) of the system is modelled by a term rewriting system and the desired properties are expressed as LTL formulas. The Maude LTL model checker is used to perform automated analysis of the system and verify non-conflicting context information guarantees it provides.

ABSTRACT. In general, system testing and verification should be conducted with respect to formal specifications. However, the development of formal specifications is a challenging and error prone task, even for experts. This is especially true when considering complex spatio-temporal requirements in real-time systems or, more generally, Cyber-Physical Systems (CPS). In this work, we present a framework for the elicitation and debugging of formal specifications. The elicitation of formal specifications is handled through a graphical user interface. The debugging algorithm checks inconsistent and inaccurate specifications. Namely, it detects validity, redundancy and vacuity issues in formal specifications developed in Metric Interval Temporal Logic (MITL). The algorithm informs the system engineers on the issues in their specifications. This improves the specification elicitation process and, ultimately, the testing and verification process. Finally, we present experimental results on specifications that typically appear in CPS applications. Application of our specification debugging tool on user derived requirements shows that the aforementioned issues are common. Therefore, the algorithm can help developers to correct their specifications and avoid wasted effort on checking the wrong requirements.

ABSTRACT. Safety-critical software-dependent systems have an increasing influence on daily life, and software malfunctioning can lead to injuries or death for humans. This is particularly relevant for medical device software whose development should adhere to certification standards. However, these standards establish general guidelines on the use of common software engineering activities without any indication regarding methods and techniques to assure safety and reliability. This paper presents a formal development process, based on the Abstract State Machine method, that integrates most of the activities required by the standards. The process permits to obtain, through a sequence of refinements, more detailed models that can be formally validated and verified. Offline and online testing techniques permit to check the conformance of the implementation w.r.t. the specification. The process is applied to the validation of the SAM medical software, that is used to measure the patients' stereoacuity in the diagnosis of amblyopia.

ABSTRACT. To manage design complexity and provide verification tractability, models of complex cyber-physical systems are typically hierarchically organized into multiple abstraction layers. High-level analysis explores interactions of the system with its physical environment, while embedded software is developed separately based on derived requirements. This separation of low-level and high-level analysis also gives hope to scalability, because we are able to use tools that are appropriate for each level. When attempting to perform compositional reasoning in such an environment, care must be taken to ensure that results from one tool can be used in another to avoid errors due to ``mismatches'' in the semantics of the underlying formalisms.

In this paper, we propose a formal approach for linking high-level continuous time models and lower-level discrete time models. Specifically, we lift a discrete-time controller specified using synchronous observer properties into continuous time for proof using timed automata (UPPAAL). To define semantic compatibility between the models, we propose a direct semantics for a network of timed automata with a discrete-time component called Contract-Extended Network of Timed Automata (CENTA) and examine semantic issues involving timing and events with the combination. We then propose a translation of the discrete-time controller into a timed automata state machine and show the equivalence of the translation with the CENTA formulation. We demonstrate the usefulness of the approach by proving that a complex medical infusion pump controller is safe with respect to a continuous time clinical scenario.

ABSTRACT. This paper proposes a modeling approach to capture the mapping of an application on a platform. The approach is based on Scenario-Aware Dataflow (SADF) models. In contrast to the related work, we express the complete design-space in a single formal SADF model. This allows us to have a compact and explorable state-space linked with an executable model capable of symbolically analyzing different mappings for their timing behavior. We can model different bindings for application tasks, different static-orders schedules for tasks bound in shared resources, as well as naturally capturing resource claiming/unclaiming using SADF semantics. Moreover, by using the inherent properties of dataflow graphs and the dynamic behavior of a Finite-State Machine, we can model different levels of pipelining, such as full application pipelining and interleaved pipelining of consecutive executions of the application. The size of the model is independent of the number of executions of the application. Since we are able to capture all this behavior in a single SADF model we can use available dataflow analysis, such as worst-case and best-case throughput and deadlock-freedom checking. Furthermore, since the model captures the design-space independently of the analysis technique, one can study and use different exploration approaches to analyze different sets of requirements.

ABSTRACT. In this paper we show a way to extract inductive-invariant from sequential circuits by analyzing only one time frame. The extraction problem is formulated with Quantified Boolean Formula which says if some relation is satisfied on the inputs coming from subsets of flipflops, the same relation must be satisfied on the outputs going to those flipflops. The QBF problem can be solved by repeatedly applying SAT solvers, which generates complete sets of test vectors for the identification of the invariant as by-product. We show that invariants on control parts of the circuits can be easily extracted from RTL HDL description even if we do not understand the behaviors that the descriptions indicate. The extracted inductive-assertions show super sets of reachable states and so can be used for logic optimization. We show that significant optimizations such 10-20% area reductions can be observed in the ISCAS89 benchmark circuits.

ABSTRACT. Chisel is a hardware construction language that supports a simplistic level of transactional programming via its Decoupled I/O primitives. In this paper we describe extensions that layer popular design paradigms on the Chisel substrate. We include RTL, SAFL-style functional hardware description, Handel-C message passing and Bluespec rules. We then briefly discuss interworking between these design styles.

ABSTRACT. Abstract--- Asynchronous circuits can be useful in many applic- ations, however, they are yet to be widely used in industry. The main reason for this is a steep learning curve for concurrency models, such Signal Transition Graphs, that are developed by the academic community for specification and synthesis of asynchronous circuits. In this paper we introduce a compositional design flow for asynchronous circuits using concepts – a set of formalised descriptions for system requirements. Our aim is to simplify the process of capturing a system requirements in form of a formal specification, and promote the concepts as a means for design reuse. The proposed design flow is applied to development of an asynchronous controller for a buck converter.

ABSTRACT. Writing test benches is one of the most frequently-performed tasks in the hardware development process. The ability to reuse common test bench features is therefore key to productivity. In this paper, we present a generic test bench, parameterised by a specification of correctness, which can be used to test any design. Our test bench provides several key features, including automatic test-sequence generation and shrinking of counter-examples, and is fully synthesisable, allowing rigorous testing on FPGA as well as in simulation. The approach is easy to use, cheap to implement, and encourages the formal specification of hardware components through the reward of automatic testing and simple failure cases.

ABSTRACT. This paper tackles the problem of testing production systems, i.e. systems that run in industrial environments, and that are distributed over several devices and sensors. Usually, such systems are not lacks of models, or are expressed with models that are not up to date. Without any model, the testing process is often done by hand, and tends to be an heavy and tedious task. This paper contributes to this issue by proposing a framework called Autofunk, which combines different fields such as model inference, expert systems, and machine learning. This framework, designed with the collaboration of our industrial partner Michelin, infers formal models that can be used as specifications to perform offline passive testing. Given a large set of production messages, it infers exact models that only capture the functional behaviours of a system under analysis. Thereafter, inferred models are used as input by a passive tester, which checks whether a system under test conforms to these models. Since inferred models do not express all the possible behaviours that should happen, we define conformance with two implementation relations. We evaluate our framework on real production systems and show that it can be used in practice.

ABSTRACT. We consider the following model repair problem: given a finite Kripke structure M and a CTL formula f, determine if M contains a substructure M' that satisfies f. That is, M can be ``repaired'' to satisfy f by deleting some transitions.

We map an instance (M,f) of model repair to a boolean formula repair(M,f) such that (M,f) has a solution iff repair(M,f) is satisfiable. Furthermore, a satisfying assignment determines which transitions must be removed from M to generate a model M' of f. Thus, we can use any SAT solver to repair Kripke structures. We also reduce satisfiability to model repair, and hence show that model repair is NP-complete.

We extend the basic repair method in several directions, as follows. (1) use abstraction: we repair a structure abstracted from M and then concretize the resulting repair to obtain a repair of M. (2) repair concurrent Kripke structures and concurrent programs: we use the pairwise method of Attie and Emerson to represent and repair the behavior of a concurrent program, as a set of ``concurrent Kripke structures'', with only a quadratic increase in the size of the repair formula. (3) repair hierarchical Kripke structures: we use a CTL formula to summarize the behavior of each ``box'', and CTL deduction to relate the box formula with the overall specification.

We have implemented the method as a GUI based tool, Eshmun.

ABSTRACT. The quality of today's embedded systems e.g. in vehicles, airplanes, or automation plants is highly influenced by their architecture. In this context, we study the so-called deployment problem. The question is where (i.e., on which execution unit) to deploy which software application or which sensor/actuator shall be connected to which device in an automation plant.

First, we introduce a domain-specific constraint and optimization language fitting the needs of our partners. Second, we investigate different approaches to tackle the deployment problem even for industrial size systems. Therefore, we present different solving strategies using (i) multi-objective evolutionary algorithms, (ii) SMT-based, and (iii) ILP-based solving approaches. Furthermore, a combination of the first two is used.

We investigate the proposed methods and demonstrate their feasibility using two realistic systems: a civil flight control system (FCS), and a seawater desalination plant. The findings of our experiments are very promising.