Designers are more and more forced to define innovative models and methodologies for managing integration of heterogeneous components and heterogeneous Chip Multiprocessors (CMPs) in modern embedded systems. In this context, component-based design seems the more promising approach, but it suffers from the lack of a widely adopted Model of Computation (MoC) able to capture component heterogeneity. This paper proposes univerCM, a new model of computation based on the Heterogeneous Intermediate Format (HIF) with the aim of supporting bottom-up design and system integration from a set of heterogeneous components. HW and SW components can be described by means of different languages and according to different MoCs, toward a uniform intermediate description based on a rigorous semantics. A mapping from univerCM to SystemC is proposed then to obtain a homogeneous description intended for fast simulation, that can be also used as starting point for CMP design flows. Experimental results show the effectiveness of univerCM in managing system heterogeneity.

Assertion-based verification (ABV) is more and more used for verification of embedded systems concerning both HW and SW parts. However, ABV methodologies and tools do not apply to HW and SW components in the same way: for HW components, both static ABV and dynamic ABV are widely used; on the contrary, SW components are traditionally verified by means of static ABV, because dynamic approaches are based on simulation assumptions which could not be true during execution of general embedded SW and which cannot be controlled by the assertion language. This paper proposes to exploit model-driven design for guaranteeing such simulation assumptions. Then, it describes an ABV framework for embedded SW, that automatically synthesizes assertion checkers to verify the embedded SW accordingly to the simulation assumptions.

Assertion-based verification (ABV) affirmed as an effective methodology for functional verification, i.e., design specification conformance, of embedded systems. Academia and industry have throughly investigated formal ABV for high-budget or safety-critical hardware and software projects, while the scalability of dynamic ABV has led to the introduction of standard languages and commercial tools addressing hardware design verification, emulation, and silicon debug. However, up to now, there were only limited studies concerning the application of dynamic ABV to embedded-software design and verification flow. We propose an analysis aiming to bridge such a gap. In particular, we illustrate how dynamic ABV can integrate and improve the various stages of the embedded-software verification flow. The analysis leads us to develop a comprehensive ABV environment that integrates the still missing automatic synthesis of executable checkers for embedded software. Experiments show that the proposed environment reduces the verification-team efforts and makes dynamic ABV practical for embedded-software design.

The relevance of formal verification methods is widely recognized in the computer science and embedded systems community. Recently, such methods have been introduced also within the control community, to help designers in developing control architectures for complex robotics systems. Robotic systems typically mix continuous and discrete behaviors that cannot be modeled faithfully using neither continuous-only nor discrete-only formalisms. The interaction of continuous and discrete dynamics makes the formal treatment of this kind of systems computationally very demanding, and justifies the need of studying new methods and algorithms. In this paper, we outline the current state-of-the-art, and describe some open problems in verification, refinement and implementation of autonomous robotic systems. We motivate the relevance of our analysis by means of an Autonomous Robotic Surgery test case.

In the last years hybrid automata have been applied in the design and verification of embedded systems. Once a hybrid model of the system has been proved to be correct with respect to the desired properties, it would be valuable to extract a correct-by-construction HW/SW implementation of it. This work discusses a methodology and a corresponding tool chain that allow to extract a HW/SW implementation of a controller modeled by a subclass of timed automata, named elastic controllers, operating in an environment represented by a hybrid automaton. The required tools have been either developed from scratch or extended from the current state-of-the-art in order to support an automated flow from hybrid automata specifications to correct-by-construction discrete implementations described in the SystemC language.

The paper tackles the problem of property qualification focusing in particular on the identification of vacuous properties. It proposes a methodology based on a combination of dynamic and static techniques that, given a set of properties defined to check the correctness of a design implementation, performs vacuity detection. Existing approaches for vacuity checking are as complex as model checking, and they require to define and model check further properties, thus increasing the verification time. Moreover, for some formulae they fail to detect vacuity, as for example in case of tautology. These problems are overcome by our approach. It is based on mutation analysis, thus, it does not require the definition of new properties granting a speed-up of the vacuity analysis process. Moreover, it provides highly accurate vacuity alerts which capture also propositional and temporal tautologies.

The paper proposes DDPSL (Drag and Drop PSL) a template library and a tool which simplifies the definition of PSL (Property Specification Language) formal properties by exploiting PSL-based templates. DDPSL allows users not expert in formal methods to define PSL properties by dragging and dropping logical and temporal operators, and variables from the design under verification (DUV) into predefined templates. Moreover, confident users or experts can extend the set of templates, reducing the effort required for formalizing complex properties. From the methodological point of view, DDPSL combines the advantages of both Open Verification Library (OVL) and PSL. Note that the templates are characterized by a parametric interface that separates the formal definition from its semantics, as provided by OVL. Moreover, the adoption of PSL as reference language guarantees the expressiveness of popular temporal logics such as Linear Temporal Logic (LTL) and Computational Tree Logic (CTL), which, on the contrary, are not fully supported by OVL. DDPSL has been successfully used to define properties for verifying an embedded application running on the microcontroller of an industrial oven.

The paper proposes a comprehensive methodology for property qualification based on a combination of dynamic and static techniques. In particular, given a set of properties defined to check the correctness of a design implementation, the methodology first evaluates property coverage, property overspecification, and it identifies vacuous properties. This is commonly performed by exploiting mutation analysis and automatic testbenches generation, i.e., dynamic strategies. This phase allows us to quickly evaluate the quality of properties with respect to the use of formal approaches. Then, a second phase, based on model checking, is applied to the restricted number of situations, where the dynamic approach is not exhaustive. Experimental results show the effectiveness and efficiency of the proposed methodology.

Vacuum cleaning is a mandatory process when an implementation is verified with respect to a specification modeled by means of formal properties. In fact, vacuum cleaning looks for properties that, passing vacuously (e.g., an implication whose antecedent is always false), may lead verification engineers to a false sense of safety. Current approaches to vacuum cleaning, generally, exploit formal methods to provide an interesting witness proving that a property does not pass vacuously. However, such approaches are as complex as model checking, and they require to define and model check further properties, thus increasing the verification time. This paper proposes an alternative approach, based on fault simulation, that requires neither the definition of new properties, nor the use of model checking. Experimental results show the high efficiency of this approach.