On the Verifiability of Programs Written in the Feature Language Extensions

High assurance in embedded system software is difficult to attain. Verification relies on testing. The unreliable and costly testing process is made much worse because the software base constantly changes: Adding a feature is by changing the code of other features, and the programs of the features entangle in the same reusable program unit of the programming language. For a large class of applications, including those requiring exception handling, this entanglement problem cannot be solved using existing general purpose programming languages. The Feature Language Extensions (FLX) is a set of language constructs designed to enable the programmer to solve the entanglement problem. It provides language support for assertion based verification. The satisfiability of first order assertions composed of variables defined by FLX can be determined without iterations of trials and errors. An executable FLX program is compiled into a finite state machine even if the state variables are unbounded.