A Functional Rephrasing of the Assumption/Commitment Specification Style

The assumption/commitment (also called rely/guarantee) style has been advocated for the specification of interactive components of distributed systems. It suggests the structuring of specifications into assumptions about the behavior of the component's environment and into commitments that are fulfilled by the component, provided the environment fulfills these assumptions. One of its motivations is to achieve modularity (also called compositionality) for state transition specifications of system components. Another reason for writing specifications in this format lies in proof rules that refer to this format. We define the assumption/commitment formats for functional system specifications. In particular, we work out a canonical decomposition of system specifications following the assumption/commitment format into safety and liveness aspects. We demonstrate the format of assumption/commitment specifications by a number of examples. Finally, we discuss the methodological significance of the assumption/commitment format in the stepwise development of specifications.     

Software auf dem Weg zur Industrialisierung

Ohne Zusammenfassung     

On the correctness of upper layers of automotive systems

Formal verification of software systems is a challenge that is particularly important in the area of safety-critical automotive systems. Here, approaches like direct code verification are far too complicated, unless the verification is restricted to small textbook examples. Furthermore, the verification of application logic is of limited use in industrial context, unless the underlying operating system and the hardware are verified, too. This paper introduces a generic model stack, allowing the verification of all system layers as well as the concrete application models being used in the upper layers. The presented models and proofs close the gap between the correctness proof for the lower layers of car electronics developed at the Saarland University and the verification procedure for distributed applications developed at the Technische Universität München.     

A uniform mathematical concept of a component

A component is a physical encapsulation of related services according to a published specification. These services can only be accessed through a consistent and published interface that includes an interaction standard. Accordingly, a component has a black box view captured by the published specification, and a glass box view showing implementation details. We claim that the following semantic model is general enough to represent all black box views of components we have discussed so far.