CSL4P: A Contract Specification Language for Platforms. Issue 3 (29th May 2017)

• Record Type: Journal Article
• Authors: Pinto, Alessandro; Sangiovanni Vincentelli, Alberto L.
• Is Part Of: Systems engineering. Volume 20:Issue 3(2017)
• Page Start: 220
• Page End: 234
• Publication Date: 2017-05-29
• Subjects: Platform‐Based -- Contract‐Based -- System Design -- Formal Methods; Systems engineering -- Periodicals; 620.0011
• DOI: 10.1002/sys.21386
• Languages: English
• ISSNs: 1098-1241

Abstract

ABSTRACT: 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 inCSL4P to provide a finer control on the semantics of interconnections. In addition, the separation of contract types from rules allows users ofCSL4P 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.