CSL4P: A contract specification language for platforms


The contract-based design formalism supports compositional design and verification, and generalizes many other languages where components are defined in terms of their assumptions and guarantees. Most languages and tools for contract-based design provide constructs to define, instantiate, and connect contracts, but fall short in capturing families of potential architectures in a flexible way. This article presents a Contract-Based Specification Language for Platforms (CSL4P). A platform comprises a set of contract types and a set of constraints called rules. Contract types can be instantiated and connected to form platform instances. While the meaning of composition is predefined in most languages, composition rules are used in CSL4P to provide a finer control on the semantics of interconnections. In addition, the separation of contract types from rules allows users of CSL4P to define different platforms out of the same set of components. This article describes syntax and semantics of the language, a development environment, which includes a compiler and a verification back-end, and an application example.

Systems Engineering