Proving that a library is backwards compatible to an older version can be challenging, as the internal representation of the libraries might completely differ and the clients of the library are usually unknown. This is especially difficult in the setting of object-oriented programs with complex heaps and callbacks. Mechanical verification is a key success factor to make such proofs practicable.

Adaptation is increasingly used in the development of safety-critical embedded systems, in particular to reduce hardware needs and to increase availability. However, composing a system from many reconfigurable components can lead to a huge number of possible system configurations, inducing a complexity that cannot be handled during system design. To overcome this problem, we propose a new component-based modeling and verification method for adaptive embedded systems. The component-based modeling approach facilitates abstracting a composition of components to a hierarchical component. In the hierarchical component, the number of possible configurations of the composition is reduced to a small number of hierarchical configurations. Only these hierarchical configurations have to be considered when the hierarchical component is used in further compositions such that design complexity is reduced at each hierarchical level. In order to ensure well-definedness of components, we provide a model of computation enabling the formal verification of critical requirements of the adaptation behavior.

Formal verification of adaptive systems allows rigorously proving critical requirements. However, design-level models are in general too complex to be handled by verification tools directly. To counter this problem, we propose to reduce model complexity on design-model level in order to facilitate model-based verification. First, we transfer existing compositional reasoning techniques for foundational models used in verification tools to design-level models. Second, we develop new compositional strategies exploiting the special features of adaptive models. Based on these results, we establish a framework for modular model-based verification of adaptive systems by model checking.

Classical specification and verification techniques support invariants for individual objects whose fields are primitive values, but do not allow sound modular reasoning about invariants involving more complex object structures. Such non-trivial object structures are common, and occur in lists, hash tables, and whenever systems are built in layers. A sound and modular verification technique for layered object structures has to deal with the well-known problem of representation exposure and the problem that invariants of higher layers are potentially violated by methods in lower layers; such methods cannot be modularly shown to preserve these invariants. We generalize classical techniques to cover layered object structures using a refined semantics for invariants based on an ownership model for alias control. This semantics enables sound and modular reasoning. We further extend this ownership technique to even more expressive invariants that gain their modularity by imposing certain visibility requirements.

Abstract We present a modular specification technique for frame properties. The technique uses modifies clauses and abstract fields with declared dependencies. Modularity is guaranteed by a programming model that enforces data abstraction by preventing representation and argument exposure, a semantics of modifies clauses that uses a notion of ‘relevant location’, and by modularity rules for dependencies. For concreteness, we adapt this technique to the Java Modeling Language, JML. Copyright © 2003 John Wiley & Sons, Ltd.

Reasoning precisely about the side effects of procedure calls is important to many program analyses. This paper introduces a technique for specifying and statically checking the side effects of methods in an object-oriented language. The technique uses data groups, which abstract over variables that are not in scope, and limits program behavior by two alias-confining restrictions, pivot uniqueness and owner exclusion. The technique is shown to achieve modular soundness and is simpler than previous attempts at solving this problem.