Enforcing design constraints with object logic

Abstract

Design constraints express essential behavioural properties of a software system. Two key elements of a scheme for enforcing design constraints are presented: a logic for describing the constraints, and an analysis that can be used both to explore the constraints in isolation (and thus gain confidence in their correctness), and to check that they are obeyed by an implementation. Examples of applications of the logic and its analysis at various levels of abstraction are given, from high-level designs to finding bugs in code. The challenge of bridging several levels, and checking code against abstract design constraints, is illustrated with a scenario from an air-traffic control system. © Springer-Verlag Berlin Heidelberg 2000.