A Formal Framework For Building, Checking And Evolving Service Oriented Architectures

Web services are often employed to create wide distributed evolvable applications from existing components that constitute a service-based software system. Services-Oriented Architectures promote loose coupling, services distribution, dynamicity and agility and introduce new engineering issues. As services involved in a SOA are remote and autonomous services, the SOA designer does not control them and unpredictable behaviour can occur. Services orchestration is a key issue in order to fit expectations and reach objectives. Thus, Service-Oriented Architectures have to be designed, analized and deployed with rigor in order to be plainly useful and quality aware. Orchestration languages (BPEL4WS, BPML, etc.) fail in some points due to the lack of formalization and expressiveness, particularly when addressing service-based architecture maintenance and evolution. This paper presents Diapason, a formal framework that allows us to formally support SOA design, ckecking, execution and evolution.