BCL: A compositional contract language for embedded systems
- Resource Type
- Conference
- Authors
- Ferrante, Orlando; Passerone, Roberto; Ferrari, Alberto; Mangeruca, Leonardo; Sofronis, Christos
- Source
- Proceedings of the 2014 IEEE Emerging Technology and Factory Automation (ETFA) Emerging Technology and Factory Automation (ETFA), 2014 IEEE. :1-6 Sep, 2014
- Subject
- Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Computing and Processing
Engineering Profession
General Topics for Engineers
Power, Energy and Industry Applications
Robotics and Control Systems
Contracts
Mathematical model
Monitoring
Software packages
Semantics
Control systems
Context
- Language
- ISSN
- 1946-0740
1946-0759
The design of large scale complex systems demands the ability to correctly specify and verify as early as possible in the design cycle the interaction of the different components that ensure that the global level requirements are satisfied. We address this issue using an approach based on the notion of contract. In particular, we propose a graphical and text-based language for requirement definition that allows designers to incrementally and hierarchically construct contract specifications for system components by composing a set of simple and intuitive patterns. The patterns have a formal semantics, and are implemented as monitor components in the Simulink framework for runtime verification. The contracts are simulated together with the components to verify both satisfaction and compatibility. A cruise control case study demonstrates the effectiveness of the approach.