Executable specifications

A system for executable specifications consists of two parts:

  • A formal specification and
  • the actual executable specification.

The formal specification describes the rules a software system should obey to. On the one hand, the rules serve as documentation of requirements, and, on the other hand, they can be formally verified to ensure functional properties. This approach lays the foundation for maximum security.

The system also provides a domain-specific language (DSL) that domain experts can use to create executable specifications. In this manner, they can directly contribute their skills. This leads to a lower error rate and thus to cost savings in troubleshooting.

The executable specification obeys the rules that were established by the formal specification. This increases the security of the software. If verification is to be carried out, formal correctness can also be guaranteed for the executable specification. A direct execution is of course possible. In this case, the executable specification is a prototype.

There is also the possibilities for code generation (eg for C/C++ or Java). The code can then be generated either in a safe manner or be tested by unit testing against the prototype.

Executable specifications also allow visualization and visual error detection as it is known from model-driven development. Documentation can also be generated.

We only use Open Source tools. Together with the use of functional programming, it becomes possible for medium-sized companies to use software with the highest quality standards.