A formal method supporting the design of fault-tolerant software

This contribution aims at supporting design for safety by means of a formal approach. The rigorous strategy developed concerns decision-making on checkpointing while processing large amounts of logical variables. The approach developed allows to implement a mechanism capable of taking appropriate decisions during execution: whether to interrupt the ongoing operation to check intermediate values, or whether to proceed and postpone the check to a later phase. In order to improve problem tractability, the application of a relatively novel data structure, namely Binary Decision Diagrams (BDDs), is recommended. In this context, the presentation will also offer a brief survey of several other efficient BDD-applications in safety engineering. (author)