Abstract
This paper studies the independent implementability of reachability properties, which are in general not compositional. We consider modal specifications, which are widely acknowledged as suitable for abstracting implementation details of components while exposing to the environment relevant information about cross-component interactions. In order to obtain the required expressivity, we extend them with marked states to model states to be reached. We then develop an algebra with both logical and structural composition operators ensuring reachability properties by construction.
A long version is available as a research report [5].
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proc. of the 9th ACM SIGSOFT Inter. Symp. on Foundations of Software Engineering (FSE 2001). pp. 109–120. ACM Press (2001)
Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating Refinement Relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bulletin of the EATCS 1(94) (2008)
Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification. Model-Checking Techniques and Tools. Springer (2001)
Caillaud, B., Raclet, J.B.: Ensuring reachability by design. Tech. rep., INRIA Research Report 7928 (2012), http://hal.inria.fr/hal-00696151
Darondeau, P., Dubreil, J., Marchand, H.: Supervisory control for modal specifications of services. In: Workshop on Discrete Event Systems (WODES 2010), Berlin, Germany, pp. 428–435 (August 2010)
Doyen, L., Henzinger, T.A., Jobstmann, B., Petrov, T.: Interface theories with component reuse. In: Proc. of the 8th Inter. Conf. on Embedded Software (EMSOFT 2008), pp. 79–88. ACM Press (2008)
Fecher, H., de Frutos-Escrig, D., Lüttgen, G., Schmidt, H.: On the Expressiveness of Refinement Settings. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 276–291. Springer, Heidelberg (2010)
Fecher, H., Schmidt, H.: Comparing disjunctive modal transition systems with an one-selecting variant. J. Log. Algebr. Program. 77(1-2), 20–39 (2008)
Feuillade, G., Pinchinat, S.: Modal specifications for the control theory of discrete-event systems. Discrete Event Dynamic Systems 17(2), 181–205 (2007)
Henzinger, T.A., Sifakis, J.: The discipline of embedded systems design. IEEE Computer 40(10), 32–40 (2007)
Larsen, K.G., Nyman, U., Wąsowski, 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)
Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: Proc. of the 5th IEEE Symp. on Logic in Computer Science, LICS 1990, pp. 108–117. IEEE Computer Society Press (1990)
Larsen, K.G.: Modal Specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990)
Larsen, K.G., Nyman, U., Wąsowski, A.: On Modal Refinement and Consistency. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 105–119. Springer, Heidelberg (2007)
Larsen, K.G., Thomsen, B.: A modal process logic. In: Proc. of the 3rd Annual Symp. on Logic in Computer Science (LICS 1988), pp. 203–210. IEEE (1988)
Lohmann, N., Wolf, K.: Compact representations and efficient algorithms for operating guidelines. Fundam. Inform. 108(1-2), 43–62 (2011)
Lynch, N., Tuttle, M.R.: An introduction to Input/Output automata. CWI-quarterly 2(3), 219–246 (1989)
Massuthe, P., Schmidt, K.: Operating guidelines - an automata-theoretic foundation for the service-oriented architecture. In: QSIC, pp. 452–457. IEEE Computer Society (2005)
Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: Modal interfaces: unifying interface automata and modal specifications. In: Proc. of the 9th Int. Conf. on Embedded Software (EMSOFT 2009), pp. 87–96. ACM (2009)
Raclet, J.B., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundam. Inform. 107, 1–32 (2011)
Wombacher, A., Mahleko, B., Neuhold, E.J.: IPSI-PF - a business process matchmaking engine based on annotated finite state automata. Inf. Syst. E-Business Management 3(2), 127–150 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Caillaud, B., Raclet, JB. (2012). Ensuring Reachability by Design. In: Roychoudhury, A., D’Souza, M. (eds) Theoretical Aspects of Computing – ICTAC 2012. ICTAC 2012. Lecture Notes in Computer Science, vol 7521. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32943-2_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-32943-2_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32942-5
Online ISBN: 978-3-642-32943-2
eBook Packages: Computer ScienceComputer Science (R0)