Supervised Synthesis

In this section, we describe the capabilities of our framework by which developers of fault-tolerance can direct the synthesis of fault-tolerant programs where automatic synthesis fails. Towards this end, we describe the user interface of the framework and the steps of the synthesis. The main menu of the framework is as follows:

  A:   Automatic 

		 S: 		Semi-automatic

		 T: 		Terminate 

		 SYNFT:>

There exist three options namely Automatic, Semi-automatic, and Terminate. The first option means that the synthesis will be performed automatically and developers have no option for the intervention during the synthesis. The Terminate option terminates the execution of the framework. And, the SYNFT:> is the command line of the framework. The Semi-automatic option provides the means for developers to conduct the synthesis of the fault-tolerant program. When developers choose this option the following menu appears.

  E:   Expand reachability graph. 

		 I: 		 Identify states from where safety of specification is violated by fault transitions.

		 R:		 Remove safety violating transitions.

		 M: 		Mark the invariant states.

		 S: 		Solve deadlock states.

		 Q: 		Query.

The first option asks the framework to generate the internal representation of the fault-intolerant program as a directed graph; i.e., reachability graph. Notice that developers have to perform the first state before moving to the subsequent steps of the synthesis. After the generation of the reachability graph, it becomes possible to choose other option in the desired order. However, in the current version of the framework, the synthesis algorithm is a deterministic implementation of the non-deterministic algorithm presented in [#!ftrtft2000!#]. Thus, it is suggested to perform the rest of the options in order. The option M results in the identification of the invariant states. The option I asks the synthesis algorithm to identify the set of states (i.e., denoted ms) from where safety of specification is violated directly by fault transitions. The identification of ms states results in the identification of a set of transitions (i.e., denoted mt) that reach a state in ms or directly violated safety. The option R asks the synthesis algorithm to remove mt transitions. The removal of mt transitions may create states that do not have any outgoing program transitions (i.e., deadlock states). The option S asks the framework to apply existing heuristics for resolving deadlock states. The complexity of synthesis mostly stems from deadlock resolution. In every subsequent step after expanding the reachability graph developers have the option to explore the reachability graph in order to understand the cause of failures of the synthesis. By selecting the option Q, developers can query the framework for particular state or transition. In the case of making a query on the states of the reachability graph, the following menu appears.

  1)   View the incoming program transitions. 

		 2) 		 View the incoming fault transitions.

		 3) 		 View the outgoing program transitions.

		 4) 		 View the outgoing fault transitions.

		 5) 		 Is this state an ms state?

		 6) 		 Is this state an invariant state?

		 7) 		 Return to the main menu.

Observe that the above menu allows developers to walk through the reachability graph in the cases where the state space is manageable. Otherwise, there exists an option to model the program being synthesized in Promela modeling language and take advantage of the SPIN model checker. Using model checkers allows developers of fault-tolerance to analyze the behaviors of the intermediate program when the synthesis of the fault-tolerant program fails. The counter examples generated by SPIN reflects the shortcomings of the existing heuristics in the synthesis of the fault-tolerant program.