SACS | A Logic for Complex Computing Systems: Properties Preservation Along Integration and Abstraction

Published in Volume XXIV, Issue 1, 2014, pages 1-46, doi: 10.7561/SACS.2014.1.1

Authors: M. Aiguier, B. Kanso

Abstract

In a previous paper [1], we defined both a unified formal framework based on L.-S. Barbosa’s components for modeling complex software systems, and a generic formalization of integration rules to combine their behavior. In the present paper, we propose to continue this work by proposing a variant of first-order fixed point modal logic to express both components and systems requirements. We establish the important property for this logic to be adequate with respect to bisimulation. We then study the conditions to be imposed to our logic (characterization of sub-families of formulae) to preserve properties along integration operators, and finally show correctness by construction results. The complexity of computing systems results in the definition of formal means to manage their size. To deal with this issue, we propose an abstraction (resp. simulation) of components by components. This enables us to build systems and check their correctness in an incremental way.

Full Text (PDF)

References

[1] M. Aiguier, F. Boulanger, and B. Kanso. A formal abstract framework for modelling and testing complex software systems. Theoretical Computer Science, 455:66–97, 2012. http://dx.doi.org/10.1016/j.tcs.2011.12.072 .

[2] M. Aiguier, B. Golden, and D. Krob. Modeling of complex systems II: A minimalist and unified semantics for heterogeneous integrated systems. Applied Mathematics and Computation, 218(16):8039–8055, 2012. http://dx.doi.org/10.1016/j.amc.2012.01.048 .

[3] M. Aiguier, B. Golden, and D. Krob. An adequate logic for heterogeneous systems. In Proceedings of the 18th International Conference on Engineering of Complex Computer Systems (ICECCS 2013), pages 65–74. IEEE Computer Society, 2013. http://dx.doi.org/10.1109/ICECCS.2013.19 .

[4] E. Alesken and R. Belcher. Systems Engineering. Prentice Hall, 1992.

[5] A. Arnold and D. Niwinski, editors. The µ-calculus over power set algebras, volume 146 of Studies in Logic and the Foundations of Mathematics, pages 141–153. Elsevier, 2001. http://dx.doi.org/10.1016/S0049-237X(01)80007-0 .

[6] L.S Barbosa. Components as processes: An exercise in coalgebraic modeling. In Proceedings of the Fourth International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000), pages 397–417, Septembre 2000. http://dx.doi.org/10.1007/978-0-387-35520-7_20 .

[7] L.S Barbosa. Towards a calculus of state-based software components. Journal of Universal Computer Science, 9(8):891–909, August 2003.

[8] M. Barr and C. Wells, editors. Category theory for computing science, 2nd ed. Prentice Hall International Ltd., Hertfordshire, UK, 1995.

[9] B.-S. Blanchard and W.-J. Fabrycky. Systems engineering and analysis. Prentice Hall, 1998.

[10] M. Bonsangue, J. M. M. Rutten, and A. Silva. Coalgebraic logic and synthesis of mealy machines. In R.M. Amadio, editor, Foundations of Software Science and Computational Structures, 11th International Conference (FOSSACS), volume 4962 of Lecture Notes in Computer Science, pages 231–245. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-78499-9_17 .

[11] J. Bradfield and C. Stirling. Modal mu-calculi. In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, pages 721–756. Elsevier, 2007.

[12] D. Cha, J. Rosenberg, and C. Dym. Fundmantals of Modeling and Analysing Engineering Systems. Cambridge University Press, 2000.

[13] H. Ehrig and H. Kreowski. Algebraic Foundations of Systems Specification, IFIP State-of-the-Art Reports, chapter Refinement and implemen- tation, pages 201–243. Springer-Verlag, 1999.

[14] J. L. Fiadeiro. Categories for Software Engineering. SpringerVerlag, 2004.

[15] H. H. Hansen, D. Costa, and J. J. M. M. Rutten. Synthesis of mealy machines using derivatives. Electronic Notes in Theoretical Computer Science, 164(1):27–45, 2006. http://dx.doi.org/10.1016/j.entcs.2006.06.003 .

[16] I. Hasuo, C. Heunen, B.Jacobs, and A. Sokolova. Coalgebraic components in a many-sorted microcosm. In Proceedings of the Third International Conference on Algebra and Coalgebra in Computer Science (CALCO 2009), Lecture Notes in Computer Science, pages 64–80, 2009. http://dx.doi.org/10.1007/978-3-642-03741-2_6 .

[17] I. Hasuo, B. Jacobs, and A. Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3(4), 2007. http://dx.doi.org/10.2168/LMCS-3)4:11+2007 .

[18] I. Hasuo, B. Jacobs, and A. Sokolova. The microcosm principle and concurrency in coalgebra. In Proceedings of the 11th International Conference on Foundations of Software Science and Computational Structures (FOSSACS 2008), volume 4962 of Lecture Notes in Computer Science, pages 246–260, 2008. http://dx.doi.org/10.1007/978-3-540-78499-9_18 .

[19] T.A. Henzinger and J.Sifakis. The discipline of embedded systems design. IEEE Computer, 40(10):32–40, 2007. http://dx.doi.org/10.1109/MC.2007.364 .

[20] C.-A.-R. Hoare. Proof of correctness of data representations. Acta Informaticae, 1(4):271–281, 1972. http://dx.doi.org/10.1007/BF00289507 .

[21] C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1985. http://dx.doi.org/10.1145/359576.359585 .

[22] J. Hughes and B. Jacobs. Simulations in coalgebra. Theoretical Computer Science, 327(1-2):71–108, 2004. doi:10.1016/j.tcs.2004.07.022 .

[23] B. Jacobs and J. Rutten. A tutorial on coalgebras and coinduction. EATCS Bulletin, 62:222-259, 1997.

[24] B. Kanso. Modeling and testing of component-based systems. PhD thesis, E´ cole Centrale Paris, 2011.

[25] B. Kanso, M. Aiguier, F. Boulanger, and C. Gaston. Testing of component-based systems. In Proceedings of the 19th Asia-Pacific Software Engineering Conference (APSEC 2012). IEEE Computer Society, 2012.

[26] R. Kashima and K. Okamoto. General models and completeness of first- order modal µ-calculus. Journal of Logic and Computation, 18(4):497–507, 2008. http://dx.doi.org/10.1093/logcom/exm077 .

[27] D. Kozen. Results on the propositional µ-calculus. Theoretical Computer Science, 27(3):333–354, 1983. doi:10.1016/0304-3975(82)90125-6 .

[28] A. Kurz. Coalgebras and modal logics. Notes of lectures given at ESSLLI’01, October 2001.

[29] E.A. Lee and S.A. Seshia. Introduction to Embedded Systems – A Cyber-Physical Systems Approach. Lee and Seshia, 2010. URL: http://chess.eecs.berkeley.edu/pubs/794.html .

[30] S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer Verlag, New York, Heidelberg, Berlin, 1971.

[31] M.-W. Maier and E. Rechtin. The art of system architecturing. CRC Press, 2002.

[32] S. Meng and L.S. Barbosa. Components as coalgebras: the refinement dimension. Theoretical Computer Science, 351(2):276–294, 2006. http://dx.doi.org/10.1016/j.tcs.2005.09.072 .

[33] R. Milner. A calculus of communicating systems. Springer-Verlag, New York, USA, 1982.

[34] R. Milner. Communication and concurrency. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1989.

[35] E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991. http://dx.doi.org/10.1016/0890-5401(91)90052-4 .

[36] D. Pattinson. Semantical Principles in the Modal Logic of Coalgebras. In H. Reichel and A. Ferreira, editors, Proceedings of the 18th Symposium on Theoretical Aspects of Computer Science (STACS 2001), volume 2010 of Lecture Notes in Computer Science, pages 514–526, 2001. http://dx.doi.org/10.1007/3-540-44693-1_45 .

[37] J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3–80, October 2000. http://dx.doi.org/10.1016/S0304-3975(00)00056-6 .

[38] A.-P. Sage and J.-E. Amstrong. Introduction to system engineering. John Wiley, 2000.

[39] Ya.-D. Sergeyev. A new applied approach for executing computations with infinite and infinitesimal quantities. Informatica, Lith. Acad. Sci., 19(4):567–596, 2008.

[40] Ya.-D. Sergeyev. Numerical computations and mathematical modelling with infinite and infinitesimal numbers. Applied Mathematics and Computing, 29(1-2):177–195, 2009. http://dx.doi.org/10.1007/s12190-008-0123-7 .

[41] J. Sifakis. A framework for component-based construction. In Proceedings of the 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM05), pages 293–299. IEEE Computer Society, 2005. http://dx.doi.org/10.1109/SEFM.2005.3 .

[42] E. Sontag. Mathematical Control Theory: Deterministic Finite Dimensional Systems, volume 6 of Textbooks in Applied Mathematics. Springer-Verlag, 1998.

[43] W.-C. Turner, J.-H. Mize, K.-E. Case, and J.-W. Nazemeth. Introduction to industrial and systems engineering. Prentice Hall, 1993.

[44] M. Viswanathan and R. Viswanathan. A higher order modal fixed point logic. In P. Gardner and N. Yoshida, editors, Proceedings of the 15th International Conference on Concurrency Theory (CONCUR 2004), volume 3170 of Lecture Notes in Computer Science, pages 512–528. Springer-Verlag, 2004. http://dx.doi.org/10.1007/978-3-540-28644-8_33 .

Bibtex

@article{sacscuza:aiguier2014alfccsppaiaa,
  title={A Logic for Complex Computing Systems: Properties Preservation Along Integration and Abstraction},
  author={M. Aiguier and B. Kanso},
  journal={Scientific Annals of Computer Science},
  volume={24},
  number={1},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2014},
  pages={1--46},
  doi={10.7561/SACS.2014.1.1},
  publisher={``A.I. Cuza'' University Press}
}