A Basic Logic for Reasoning about Connector Reconfiguration

• Autorzy: Clarke D.
• Języki publikacji: EN

Abstrakty

EN

Software systems evolve over time. From a component-based software engineering perspective, this means that either the components of the system need to change, or, if components are connected using a coordination layer, then the way in which they are connected needs to change, or both. In some situations, changes must be performed without stopping the running system. This not only introduces a serious technological challenge, it also makes reasoning about the evolving system difficult. One approach to this problem is to use component connectors to plug components together. Reconfiguration of a system can then be reduced to reconfiguring the component connector, as changing component implementations can be implemented by changing which components the connector connects together. The coordination language Reo offers operations to dynamically reconfigure the topology of component connectors, but until now, no means for reasoning about reconfiguration in Reo has been developed. This issue is addressed in this paper. To enable reasoning about connector behaviour, and hence behaviour of the composed system, we present a semantics of Reo in the presence of reconfiguration, and a logic together with its model checking algorithm.

Słowa kluczowe

EN

dynamic reconfiguration; coordination; component connectors; Reo

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 82, nr 4
• Strony: 361--390
• Opis fizyczny: bibliogr. 46 poz., wykr.

Twórcy

autor

Clarke D.

• CWI, Kruislaan 413, NL-1098 SJ, Amsterdam, the Netherlands,

Bibliografia

• [1] Abdulla, P. A., Baier, C., Iyer, S. P., Jonsson, B.: Reasoning about Probabilistic Lossy Channel Systems, CONCUR '00: Proceedings of the 11th International Conference on Concurrency Theory, Springer-Verlag, London, UK, 2000, ISBN 3-540-67897-2.
• [2] Arbab, F.: Reo: A Channel-based Coordination Model for Component Composition, Mathematical Structures in Computer Science, 14(3), June 2004, 329-366.
• [3] Arbab, F.: Abstract Behavior Types: a foundation model for components and their composition, Science of Computer Programming, 55, 2005, 3-52.
• [4] Arbab, F., Baier, C., de Boer, F., Rutten, J.: Models and Temporal Logics for Timed Component Connectors, IEEE International Conference on Software Engineering and Formal Methods (SEFM '04), IEEE Computer Society, Beijing, China, September 2004, ISBN 0-7695-2222-X.
• [5] Armstrong, J., Williams, M., Wikstrom, C., Virding, R.: Concurrent Programming in Erlang, Prentice-Hall, New Jersey, USA, 1996.
• [6] Arndol, A.: Finite Transition Systems, Prentice Hall, 1994.
• [7] Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata, Science of Computer Programming, 61(2), 2006, 75-113, ISSN 0167-6423.
• [8] Baltag, A., Moss, L. S., Solecki, S.: A logic of public announcements, common knowledge, and private suspicions, Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge (TARK-98), Evanston, IL, USA (I. Gilboa, Ed.), Morgan Kaufmann, 1998.
• [9] Beer, I., Ben-David, S., Landver, A.: On-the-FlyModel Checking of RCTL Formulas, CAV '98: Proceedings of the 10th International Conference on Computer Aided Verification, number 1427 in Lecture Notes in Computer Science, Springer-Verlag, London, UK, 1998, ISBN 3-540-64608-6.
• [10] van Bentham, J.: An essay on sabotage and obstruction, Festschrift in Honour of J¨org Siekman (D. Hutter, S. Werner, Eds.), number 2605 in Lecture Notes in Computer Science, 2005.
• [11] Bergstra, J., Klint, P.: The discrete time ToolBus - A software coordination architecture, Science of Computer Programming, 31(2-3), July 1998, 205-229.
• [12] Berry, G.: The Foundations of Esterel, in: Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, 2000, 425-454.
• [13] Bettini, L., Nicola, R. D., Loreti, M.: Formalizing Properties of Mobile Agent Systems, Coordination Languages and Models, number 2315 in Lecture Notes in Computer Science, 2002.
• [14] Bierman, G., Hicks, M., Sewell, P., Stoyle, G., Wansbrough, K.: Dynamic rebinding for marshalling and update, with destruct-time _, International Conference on Functional Programming (ICFP), August 2003.
• [15] Bruni, R., Lanese, I., Montanari, U.: A Basic Algebra of Stateless Connectors, Theoretical Computer Science, 366(1-2), November 2006, 98-120.
• [16] Cardelli, L., Gordon, A. D.: Ambient Logic, Mathematical Structures in Computer Science, 2005, To Appear.
• [17] Clarke, D. G.: Reasoning about connector reconfiguration I: Equivalence of constructions, Technical Report SEN-R0506 ISSN 1386-369X, CWI, Amsterdam, The Netherlands, 2005.
• [18] Clarke, D. G.: Reasoning about Connector Reconfiguration II: Basic Reconfiguration Logic, IPM International Workshop on Foundations of Software Engineering (FSEN'05) (F. Arbab, M. Sirjani, Eds.), number 159 in ENTCS, Elsevier, 2005.
• [19] Clarke, D. G., Costa, D., Arbab, F.: Modelling Coordination in Biological Systems, Int. Symposium on Leveraging Applications of Formal Methods (ISoLA 2004), number 4313 in Lecture Notes in Computer Science, Springer-Verlag GmbH, October 2006.
• [20] Clarke, E., Jha, S., Lu, Y., Veith, H.: Tree-Like Counterexamples in Model Checking, Logic in Computer Science, 2002, 19-26, ISSN 1043-6871.
• [21] Clarke Jr., E. M., Grumberg, O., Peled, D. A.: Model Checking, MIT Press, 1999.
• [22] Clavel, M., Dur´an, F., Eker, S., Lincoln, P., Mart´ı-Oliet, N., Meseguer, J., Quesada, J. F.: Maude: Specification and Programming in Rewriting Logic, Theoretical Computer Science, 285, August 2002, 187-243.
• [23] Demartini, C., Iosif, R., Sisto, R.: dSPIN: A Dynamic Extension of SPIN, Theoretical and Practical Aspects of SPIN Model Checking (D. Dams, R. Gerth, S. Leue, M. Massnik, Eds.), number 1680 in Lecture Notes in Computer Science, Springer, 1999.
• [24] Distefano, D.: On model checking the dynamics of object-based software: a foundational approach, Ph.D. Thesis, University of Twente, Nov 2003.
• [25] Ducasse, S., Hofmann, T., Nierstrasz, O.: OpenSpaces: An object-oriented framework for reconfigurable coordination spaces, Coordination Languages and Models, number 1906 in Lecture Notes in Computer Science, September 2000.
• [26] Farwer, B.: Dynamic modification of object Petri nets: an application to modelling protocols with fork-join structures, Fundamenta Informaticae, 51(1), 2002, 91-101, ISSN 0169-2968.
• [27] Farwer, B., Misra, K.: Dynamic Modification of System Structures Using LLPNs, Proceedings of Andrei Ershov Fifth International Conference PERSPECTIVES OF SYSTEM INFORMATICS, number 2890 in Lecture Notes in Computer Science, July 2003.
• [28] Ghassemi, F., Tasharofi, S., Sirjani, M.: Automated mapping of Reo circuits to constraint automata, IPM International Workshop on Foundations of Software Engineering (FSEN'05) (F. Arbab, M. Sirjani, Eds.), number 159 in ENTCS, Elsevier, 2005.
• [29] Girault, C., Valk, R., Eds.: Petri Nets for Systems Engineering, Springer-Verlag, 2003.
• [30] Guillen-Scholten, J., Arbab, F., de Boer, F. S., Bonsangue, M. M.: Modeling the Exogenous Coordination of Mobile Channel-based Systems with Petri Nets., FOCLASA, number 154 in ENTCS, 2006.
• [31] Hirsch, D., Inveradi, P.,Montanari, U.: Reconfiguration of Software Architecture Styles with NameMobility, Coordination Languages and Models, number 1906 in Lecture Notes in Computer Science, September 2000.
• [32] Holzmann, G. J.: The SPIN Model Checker, AddisonWesley, 2003.
• [33] Milner, R.: Communicating and Mobile Systems: the Pi-Calculus, Springer Verlag, 1999.
• [34] Nicola, R. D., Fantechi, A., Gnesi, S., Ristori, G.: An Action-Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems., Computer Networks and ISDN Systems, 25(7), 1993, 761-778.
• [35] Papadopoulos, G. A., Arbab, F.: Coordination models and languages, M. Zelkowitz (Ed.), The Engineering of Large Systems, 46, Academic Press, 1998.
• [36] Papadopoulos, G. A., Arbab, F.: Configuration and dynamic reconfiguration of components using the coordination paradigm, Future Generation Computer Systems, 17, 2001, 1023-1038.
• [37] Petri, C. A.: Kommunikation mit Automaten, Ph.D. Thesis, University of Bonn, 1962.
• [38] Rabinovich, A.: Quantitative analysis of probabilistic lossy channel systems, Inf. Comput., 204(5), 2006, 713-740, ISSN 0890-5401.
• [39] Stehr, M.-O., Meseguer, J., ¨Olveczky, P. C.: Rewriting Logic as a Unifying Framework for Petri Nets, Unifying Petri Nets (Advances in Petri Nets) (H. Ehrig, G. Juhas, J. Padberg, G. Rozenberg, Eds.), number 2128 in Lecture Notes in Computer Science, Springer-Verlag, 2001.
• [40] Valk, R.: Petri Nets as Token Objects: An Introduction to ElementaryObject Nets, ICATPN '98: Proceedings of the 19th International Conference on Application and Theory of Petri Nets, number 1420 in Lecture Notes in Computer Science, Springer-Verlag, London, UK, 1998, ISBN 3-540-64677-9.
• [41] Verbaan, P. R. A., van Leeuwen, J., Wiedermann, J.: Lineages of automata, Technical Report UU-2004-018, Utrecht University: Information and Computing Sciences, 2004.
• [42] Wong, S. K. M., Wang, L. S., Yao, Y. Y.: Interval structure: a framework for representing uncertain information, Proceedings of the Eighth conference on Uncertainty in Artificial Intelligence, Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1992, ISBN 1-55860-258-5.
• [43] Yahav, E., Reps, T. W., Sagiv, S., Wilhelm, R.: Verifying Temporal Heap Properties Specified via Evolution Logic., ESOP (P. Degano, Ed.), number 2618 in Lecture Notes in Computer Science, Springer, 2003.
• [44] Yao, Y. Y., Lin, T. Y.: Generalization of rough sets using modal logic, Intelligent Automation and Soft Computing, 2, 1996, 103-120.
• [45] Yellin, D. M., Strom, R. E.: Protocol specifications and component adaptors, ACM Trans. Program. Lang. Syst., 19(2), 1997, 292-333, ISSN 0164-0925.
• [46] Zlatev, Z., Diakov, N., Pokraev, S.: Construction of Negotiation Protocols for E-Commerce Applications, ACM SIGecom Exchanges, 5(2), November 2004, 12-22.