A Modal Interface Theory with Data Constraints - Formal Methods: Foundations and Applications - page 95

specification transitions with pre- and postconditions, the implementation must
guarantee that single specification transitions of a component are executed in an
atomic way.
Verification techniques for refinement and compatibility are clearly an impor-
tant issue for future work. Further next steps are, from the theoretical point of
view, to extend our framework by taking into account weak versions of refine-
ment and compatibility abstracting away not only internal actions, as done for
MIOs in [10,4], but also internal state variables. From the practical point of view
we plan to integrate data constraints in our tool, the MIO Workbench [4], for
modal refinement and compatibility checking.
References
1. Barros, T., Ameur-Boulifa, R., Cansado, A., Henrio, L., Madelaine, E.: Behavioural
models for distributed Fractal components. Annales des Telecommunications
64(1-2), 25-43 (2009)
2. Bauer, S.S., Hennicker, R., Bidoit, M.: A modal interface theory with data
constraints. Technical Report 1005, Ludwig-Maximilians-Universitat Munchen,
Germany (2010)
3. Bauer, S.S., Hennicker, R., Janisch, S.: Behaviour protocols for interacting stateful
components. Electr. Notes Th. Comp. Sci. 263, 47-66 (2010)
4. Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility,
refinement, and the MIO Workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS
2010. LNCS, vol. 6015, pp. 175-189. Springer, Heidelberg (2010)
5. Bidoit, M., Hennicker, R., Knapp, A., Baumeister, H.: Glass-box and black-box
views on object-oriented specifications. In: Proc. SEFM 2004, Beijing, China, pp.
208-217. IEEE Comp. Society Press, Los Alamitos (2004)
6. de Alfaro, L., Henzinger, T.A.: Interface Theories for Component-Based Design.
In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp.
148-165. Springer, Heidelberg (2001)
7. Fernandes, F., Royer, J.-C.: The STSLib project: Towards a formal component
model based on STS. Electr. Notes Th. Comp. Sci. 215, 131-149 (2008)
8. Fischer, C.: CSP-OZ: a combination of Object-Z and CSP. In: Proc. FMOODS,
Canterbury, UK, pp. 423-438. Chapman and Hall, Boca Raton (1997)
9. Larsen, K.G., Nyman, U., Wasowski, A.: Modal I/O Automata for Interface and
Product Line Theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp.
64-79. Springer, Heidelberg (2007)
10. Larsen, K.G., Nyman, U., Wasowski, A.: On Modal Refinement and Consistency.
In: Caires, L., Li, L. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 105-119. Springer,
Heidelberg (2007)
11. Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: 3rd Annual Symp. Logic in
Computer Science, LICS 1988, pp. 203-210. IEEE Computer Society, Los Alamitos
(1988)
12. Mouelhi, S., Chouali, S., Mountassir, H.: Refinement of interface automata
strengthened by action semantics. Electr. Notes Theor. Comput. Sci. 253(1),
111-126 (2009)