PARallel program DESigner (PARDES):

 A Framework for Action-Level Compositional Design of the Behavioral Evolution of Parallel Programs

Program behaviors evolve often due to incomplete specifications and unanticipated requirements. Designing the behavioral evolution of parallel programs is difficult in part due to inherent non-determinism of such programs. In our previous work, we have formulated the behavioral evolution of finite-state parallel programs in terms of adding Linear Temporal Logic (LTL) properties to existing programs, where we revise an existing program in order to satisfy a new (safety or liveness) property while preserving existing properties.  We extend our work by presenting a novel approach for decomposing the addition problem to the level of program actions, called action-level addition. In the proposed approach, we separately analyze and revise the actions of an existing program in order to accommodate a new property while preserving already existing properties. Our proposed approach has important applications in distributed model checking and model-driven development as well. Specifically, in model checking, we distribute the actions of a program on network of machines where the actions are analyzed separately so the entire analysis will result in verifying the entire program for a specific LTL property. Our approach provides the option to go one step beyond model checking by providing corrective suggestions to developers. We have implemented our action-level method in an extensible software framework, called PARallel program DESigner (PARDES), that exploits the computational resources of distributed machines for the addition of LTL properties. For more information on PARDES, please click here.