A System for Predictable Component-Based Software Construction

Large systems are invariably built from assembled components. It is essential for such systems to have predictable behavior, if the risks of failure are too high. To enable practical and modular verification of industrial-strength systems, software practitioners need to learn to build both behavioral specifications of components and component implementations that are annotated with suitable internal assertions. Neither of these tasks can be automated, in general. However, once suitable specifications and implementations of components are given, a mechanical system (with human assistance) can check in a modular and scalable fashion if component-based software behaves as specified. To illustrate the issues, the paper presents a non-trivial component-based example. The example underscores that predictable component-based construction is challenging, and that it cannot become practical, without educating students and software developers on principles of mathematical specifications and correct, efficient implementations.

Keywords

• Software Reuse

• Predictable Behavior

• Abstraction Relation

• Minimal Linkage

• Reusable Software Component

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.