Formal Specification of COTS-Based Software: A Case Study

摘要

Reusable commercial off-the-shelf (COTS) products are routinely employed in development of software systems. However, no systematic techniques are available for specification or verification of critical aspects of such systems. This paper explains that the dependencies between a critical subsystem and a COTS product can be isolated through formally-stated mathematical and programmatic interface contracts. The contracts allow specification and reasoning of critical subsystems, without a need to describe entire COTS product functionality formally. They also provide the flexibility of using alternative COTS products that include the desired behavior. The paper illustrates elements of the proposed approach using a subsystem of the NASA/FAA Surface Movement Advisor (SMA). The subsystem is based on a COTS database.