Contract platform and tools

This paper describes a specification language for platforms using contracts. We provide the intuitive explanation of what a contract-based platform is as well as the formal analysis. By using Satisfiability Modulo Theories tools, architectures or detailed designs derived from such platforms can be verified automatically. A tool is presented that allows users to design platform components and rules and verify designs based on such platforms. The tool also assists users to identify possible design changes that enable automatic verification. The approach is illustrated using an example electrical power system.