Title

Formal Verification of Hybrid Continuous-Time/Discrete-Time (CT/DT) Systems Using Model Checking and Satisfiability-Modulo-Theory (SMT) Solving

Keywords

Hybrid Automata, Cyber-Physical Systems, Model Checking, SMT, Nonlinear Systems

Description

Present embedded and cyber-physical systems show an increasing degree of complexity and heterogeneity, which results in severe challenges in their design and verification process. This trend has motivated the introduction of formalisms that are able to contemporarily capture discrete and continuous dynamics, e.g. hybrid automata, and non-linear behaviors. While the simulation of these models is currently becoming affordable, formal techniques of verification are still at an early stage of development.

We have recently proposed an approach to the verification of these models: our framework, CalCS, can contemporarily capture discrete and continuous dynamics, while including non-linear behaviors.  A hybrid CT-DT system is first modeled using the formalism of hybrid automata, where non-linear expressions are convex [1]. The model is then verified using techniques from Bounded Model Checking (BMC) and SMT solving, which have shown to be effective in the verification of discrete systems. While problems including non-linear arithmetic constraints over the real numbers can soon become non-tractable in general, CalCS can reason about combinations of convex constraints using results from optimization theory.

In this project, the student will build up on the proposed approach by applying it to the verification of a real (complex) system. In particular, the project can be divided into the following sub-tasks:

1.       Modeling of a real system within the proposed framework. The system should be characterized by a non-linear behavior that can be captured using convex (and concave) expressions. Moreover, the system should present both discrete and continuous dynamics.

2.       Verification of the system using CalCS.

3.       Comparison with other state-of-the-art tools, to assess the strength and weakness points of the proposed approach, in terms of expressivity, scalability and accuracy.

Although the real system to be modeled can be chosen arbitrarily, we suggest the study of an Analog Mixed Signal (AMS) Integrated Circuits (ICs) [2], e.g. data converter (ADC/DAC), PLL, Switched Capacitor (SC) filter. These systems inherently show a high level of heterogeneity in their dynamics, and the non-linear component of their behavior is increasingly becoming dominant in the characterization of their performance, e.g. reliability. Hence, AMS-ICs represent a relevant example of application of the proposed approach.

Mentors

Pierluigi Nuzzo (nuzzo AT eecs.berkeley.edu), Alberto Puggelli (puggelli AT eecs.berkeley.edu)

Required knowledge:

Basic knowledge of the techniques used in the verification of discrete systems; some familiarity with MATLAB and C++.

Readings:

[1] Pierluigi Nuzzo, Alberto Puggelli, Sanjit A. Seshia, and Alberto L. Sangiovanni-Vincentelli, “CalCS: SMT Solving for Non-linear Convex Constraints,” In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2010. To appear. See: http://www.eecs.berkeley.edu/~sseshia/pubs/b2hd-nuzzo-fmcad10.html.

[2] D. Walter, S. Little, and C. Myers, “Bounded model checking of analog and mixed-signal circuits using an SMT solver,” in AutomatedTechnology for Verification and Analysis, 2007, pp. 66–81.

Title

Behavioral Modeling for Platform-based Design of Mixed-Signal (Analog/Digital) Integrated Systems Using Contracts

Keywords

Analog and Mixed-Signal Integrated Circuits, Contract-based Design.

Description

The complexity of today's embedded electronic systems as well as their demanding performance and reliability requirements are such that their design can no longer be tackled with ad hoc techniques while still meeting tight time-to-market constraints. To boost productivity and enforce design correctness and robustness, a rigorous design discipline is a crucial target, which also relies on hierarchical design-space exploration, as well as compositional methods, to achieve efficient and high-quality system-level design. However, in analog electronic systems, circuit behaviors are so tightly dependent on their interface conditions that accurate system performance estimations based on characterizations of individual stand-alone circuits is a hard task. Since there is no general solution to this problem, analog system integration has traditionally been heavily dependent on designers' experience.

We have proposed an approach to the design of mixed-signal systems that builds upon the analog platform-based design methodology [1] by exploiting contracts to enforce correct-by-construction system-level composition. Contracts intuitively capture the thought process of a designer, who aims at guaranteeing circuit performance only under specific assumptions (e.g. loading and dynamic range) on the interface properties, and they have shown to be promising when applied to the design of an ultra-wide band receiver front-end [2]. In this project, the student will build up on the existing framework by applying it to model key components of today’s mixed-signal Systems-on-Chip (SoC), such as a DC-DC converter for power management applications, or a Phase-Locked-Loop (PLL) for clock generation. Possible articulation phases of this project include:

1.       Selection of one or, possibly, more circuit topologies for the target application and platform;

2.       Extraction of an executable behavioral model for efficient system-level exploration using SystemC and its recent AMS extensions;

3.       Model validation by comparison with lower level (up to transistor-level) descriptions of the component in terms of scalability and accuracy.

Mentors

Pierluigi Nuzzo (nuzzo AT eecs.berkeley.edu), Alberto Puggelli (puggelli AT eecs.berkeley.edu), Xuening Sun (xuening@eecs.berkeley.edu)

Required knowledge:

Some familiarity with MATLAB, and inclination in dealing with physical aspects in embedded system design. No previous knowledge of SystemC is required for this project; getting familiar with the modeling language is part of the learning process during its development.  

Readings:

[1] Pierluigi Nuzzo, Xuening Sun, Chang-Ching Wu, Fernando De Bernardinis, and Alberto Sangiovanni-Vincentelli, “A Platform-Based Methodology for System-Level Mixed-Signal Design,” EURASIP Journal on Embedded Systems, vol. 2010, Article ID 261583, 14 pages, 2010. doi:10.1155/2010/261583

[2] Xuening Sun, Pierluigi Nuzzo, Chang-Ching Wu and Alberto Sangiovanni-Vincentelli, "Contract-based system-level composition of analog circuits," Proc. of Design Automation Conference 2009, pp. 605-610, July 2009.

Title

Semantics Preservation in the Implementation of Synchronous Reactive Models over Synchronous and Loosely Asynchronous Architectures

Category

Design Tools

Description

Future automobiles are required to support an increasing number of complex, distributed functions such as active safety and X-by-wire. Because of safety concerns and the need to deliver correct designs in a short time, system properties should be verified in advance on function models, by simulation or model checking. To ensure that the properties still hold, the implementation of the models into a distributed platform, consisting of a set of nodes connected by one or more networks and a software implementation of tasks and communication messages, should preserve properties of the model (in general, its semantics). We are especially interested in extending previous analysis on single-cpu platform [1] to distributed time-triggered systems such as FlexRay-based architectures [2] or LTTA platforms.

FlexRay [3] as a time-triggered communication protocol offers the possibility of deterministic communication and can be used to define distributed implementations that are provably equivalent to synchronous reactive models like those created from Simulink. However, the low level communication layers and the FlexRay schedule must be carefully designed to ensure the preservation of communication flows and functional outputs. In [2], we provide a discussion of the impact of such constraints on the task and message scheduling. When the scheduling problem is not feasible, an additional layer is added to the problem, which includes the possible tradeoffs between schedulability and additional functional delays in the controls and the question becomes: what is the (optimal) feasible solution that preserves the communication semantics on selected links and optimizes the system performance? The project can be further extended by generalizing the mapping into a more general class of susyems: Loosely Time-Triggered Platforms. For such platforms, a general mapping framework has been presented in [4], however, with serious limitations for the time analysis (exceedingly pessimistic) and the applicability. Recent results [5] provide the foundation for improving the time analysis in [4] and improve the condition for correct mapping.

Mentors

Haibo Zeng (haibo.zeng AT gm.com), Marco Di Natale (marco AT sssup.it)

Required knowledge:

Strong programming and software engineering experience.

Readings:

[1] M. Di Natale, L. Guo, H. Zeng, and A. Sangiovanni-Vincentelli. Synthesis of Multi-task Implementations of Simulink Models with Minimum Delays. IEEE Transactions on Industrial Informatics.

[2] M. Di Natale and H. Zeng. Time determinism and semantics preservation in the implementation of distributed functions over FlexRay. In SAE Word Congress, 2010

[3] Flexray consortium, Protocol Specification V2.1 Rev. A, available at http://www.flexray.com, 2006.

[4] S. Tripakis, C. Pinello, A. Benveniste, A. Sangiovanni-Vincentelli, P. Caspi and M. Di Natale “Implementing Synchronous models on Loosely Time-Triggered Architectures”, IEEE Transactions on Computer, October 2008, Volume 57 Issue 10.

[5] A. Bouillard, L. T.X. Phan and S. Chakraborty, Lightweight Modeling of Complex State Dependencies in Stream-Processing Systems, 15th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), San Francisco, California, Apr 2009.

Title

Work on integration of two component-based design frameworks.

Category

Design Tools

Description

System level analysis plays an essential role in the early stage design of all types of embedded systems. Several different methodologies that address the problem of various system level analyses of different embedded systems have been presented recently. This project will require a student or a group of students to study and work with two of the leading frameworks that support the idea of component-based design. This work will be considered as a part of the European COMBEST project.

The objective of the project is to combine the functional specification of the BIP framework with the architecture exploration capabilities of the Metro II framework. This is done by integrating the BIP model into Metro II, and by replicating the BIP interaction paradigm using the Metro II primitives.

The Behavior-Interaction-Priority (BIP) framework is developed at the VERIMAG laboratory in Grenoble, France. Briefly, a system specification in BIP is divided in three layers. At the bottom layer, the behavior of the system is specified as a collection of independent finite state transition systems (components), which communicate with the environment through ports. Each transition of a component is activated by an interaction, which is a subset of its ports. At the middle layer, a set of connectors specifies the possible interactions of the components. The third layer is represented by interaction priorities. One of the strengths of the BIP framework is the ability to check certain properties, such as deadlock-freedom, in a compositional way. This is obtained at the expense of a more complex coordination scheme, involving the connectors, which must determine the global set of possible interactions. This may adversely impact simulation performance, and, for certain communication paradigms may require a number of connectors that grows exponentially with the number of components.

Metro II, developed at UC Berkeley, is also concerned in global properties, but focuses on those that have to do with the resource consumption of the architecture. The quantities associated with these properties are determined using specific annotators and schedulers are used to coordinate the execution. Schedulers can be seen as a form of connector, since they regulate the execution of the system. Metro II provides more flexibility in the interaction models, although this may come at the cost of lower formal analysis capabilities.

In this project we propose to develop an automatic translation path from deadlock free functional BIP models into Metro II components. This path has already been demonstrated on manual examples. The translation requires that specific schedulers and constraints be developed in Metro II, while the C code generated by BIP is potentially adapted to the Metro II component interface. A case study should be developed to demonstrate the functionality of the integration.

The students involved in the project will learn about various coordination mechanisms and how these can be implemented using both executable and declarative methods. The students will have hands on experience on the workings of architecture exploration tools. Knowledge of C/C++ is required

Mentors

Alena Simalatsar (University of Trento, e-mail: simalats AT disi.unitn.it )

Required knowledge:

Strong programming and software engineering experience.

Readings: