Tutorial on Property-Based and Contract-Based Design of System Architectures (ASE13)

General information

  • Location: Crowne Plaza Cabana Hotel, Palo Alto, CA
  • Time: Tuesday, 12th of November 2013 in the afternoon
  • Registration: see ASE'13 registration website

Abstract

Model-based system engineering has been introduced to cope with the growing complexity of safety-critical systems. Some of the major concerns in model-based system engineering is to properly formalize the system properties and to design the system architecture so that the components are integrated in order to satisfy the system properties. Property-based approaches to system design focus on properties (rather than on behavioral models) and analyze the system properties to find errors very early in the design process, much before the components are implemented. Property specification languages are typically based on temporal logics and have been enriched to take into account real-time and safety aspects. In contract-based design, properties are structured into assumptions and guarantees to specify the properties on component interfaces. First conceived in the context of object-oriented programming, contract-based design is now applied also to the architecture of embedded systems. Contract-based design provides an ideal paradigm for a correct design of system architecture, with a clear description of the expected interaction of each component with its environment. This enables compositional reasoning, independent refinement and a proper reuse of components. The tutorial will introduce the concepts of property- and contract-based design for component-based system architectures in the context of embedded systems. The first part of the tutorial will give an overview of standard languages to describe system properties and architectures and formally define the concept of component interfaces and their semantics. The second part will focus on the contract-based framework provided by the OCRA tool, the property specification language used by OCRA, its support for the specification and verification of contracts refinement, and its usage within the modeling environments of CASE tools.

Outline

The tutorial will be split into two main parts, the first one focused on the methodologies and formal aspects, the second focused on the proposed concrete language and tool. The tutorial will be organized according to the following outline:

  1. First part
    • Introduction and motivations
    • Component interfaces and system architectures
    • Properties and temporal logics
    • Contract-based system design
      • Contracts refinement
      • Compositional verification and reuse
      • Contract-based fault-tree analysis
  2. Second part
    • OCRA language
    • OCRA tool
    • Related CASE tools
    • Case studies

Slides

Here you may find the slides and the OCRA examples presented during the tutorial.