Using Process Algebra to Validate Behavioral Aspects of Object-Oriented Models

We present in this paper a rigorous and automated based approach for the behavioral validation of control software systems. This approach relies on metamodeling, model-transformations and process algebra and combines semiformal object-oriented models with formal validation. We perform the validation of behavioral aspects of object-oriented models by using a projection into a welldefined formal technical space (Finite State Process algebra) where model-checkers are available (we use LTSA; a model checker for Labeled Transition Systems). We then target an implementation platform, which conforms to the semantics of the formal technical space; in turn, this ensure conformance of the final application to the validated specification. 1 Inroduction The increasing complexity of control software systems makes their comprehension and their construction more and more difficult [11]. The approach proposed in this paper (figure 1) simplifies the reliable design of these software systems through a c...

• Type: Conference
• Year: 2005
• Where: UML
• Authors: Alban Rasse, Jean-Marc Perronne, Pierre-Alain Muller, Bernard Thirion
• Keywords: Control Software Systems, Formal Technical Space, Natural Language Processing, Software Development Cycle, UML 2005