In spite of recent developments, formal methods are still not widely used in practice, mostly because of their complexity and need for special training. This situation may be remedied by a formal method that hides the complexity from its user, the software developer.

For verification of real-time systems, the authors of this paper introduce temporal skeletons, a graphical formal notation for real-time models. Temporal skeletons can be derived from the application source code (in Ada), and their key achievement is their minimal complexity. As their structure follows the structure of the source code, even developers who are not experts in formal methods should hopefully be able to validate whether they properly model the application.

Several features of temporal skeletons contribute to their low complexity. The principal one is the grouping of passive instructions into passive blocks. Even a large section of sequential code may be represented by only a single passive block in the temporal skeleton. The skeletons may be optionally annotated with additional information (which the paper unfortunately does not elaborate on) to be used in generating a more specific model for the verification backend (UPPAAL [1] is the choice of the authors). UPPAAL then verifies the model of the whole system, constructed by merging the application model with the model of the kernel. Through the option of automatic re-extraction of the skeletons from the code, this approach overcomes the struggle of keeping the model consistent with the code, and has the potential to make formal verification more accessible.