The goal of this work package is to develop new techniques and the underlying theories to support the design and the implementation of correct and reliable service components (SC) and service component ensembles (SCE). We have worked in several different directions in order to get closer to our goal. Our contributions can be grouped into the following main directions:

1. We have presented a new and flexible approach to repair reactive programs with respect to a specification.
2. We have developed a semi-symbolic algorithm for synthesizing controllers in a stochastic environment, implemented as an add-on to the probabilistic model checker PRISM. 
3. We have presented a new method for generating linear invariants for SC. In particular we developed an incremental approach that allows discovering and reusing invariants that have been already been computed on subparts of the model. These new techniques have been implemented in D-Finder, a tool for checking deadlock freedom. 
4. We propose an approach to make the specification of access control policies accessible to people not necessarily familiar with formal languages. We propose the model-driven process shown in the figure below.
5. We propose a formal pattern-based approach to study defense mechanisms against DoS attacks. We enhance pattern descriptions with for- mal models that allow the designer to give guarantees on the behavior of the proposed solution. 
6. Finally, we developed and extension of GMC with support of C++. Also, we have created a local version of the jDEECo framework.

Contact: Saddek Bensalem  This e-mail address is being protected from spambots. You need JavaScript enabled to view it