Modeling and Formal Verification of Component-Based Information Systems
Abstract
This paper describes the application of a framework named COMPOR-CPN to the formal modelling and verification of component based information systems. The framework is a Colored Petri Net modelling of the COMPOR component model specification. We describe the usage of the COMPORCPN to model and verify an information system for managing virtual communities.
Keywords:
Framework, COMPOR-CPN, Information systems, Colored Petri Nets
References
Almeida, H. O., de Barros Costa, E., Barbosa, N. M., Bublitz, F. M., and de Andrade Barbosa, A. (2004a). Um Arcabouço de Software Livre baseado em Componentes para a Construção de Ambientes de Comunidades Virtuais de Aprendizagem na Web. In Anais do XV Simposio Brasileiro de Inform atica na Educac ¸ao SBIE’05 , pages 188– 196, Manaus, Amazonas, Brasil.
Almeida, H. O., Perkusich, A., Paes, R. B., and Costa, E. B. (2004b). Composição Dinâmica de Componentes para Aplicaç ões com Mudanças Frequëntes de Requisitos. In Anais do 4o Workshop de Desenvolvimento Baseado em Componentes, pages 9–14, João Pessoa, Paraıba, Brasil.
Aniorte, P. (2003). Componet-Based Software Development: From Component Model to Software Architecture. In ICSR7 2002 Workshop on Component-based Software Development Processes, Austin, Texas, USA.
Bernd Finkbeiner and Ingolf Kr¨uger (2001). Using Message Sequence Charts for Component-Based Formal Verification. In Giannakopoulou, D., Leavens, G. T., and Sitaraman, M., editors, SAVCBS 2001 Proceedings: Specification and Verification Component-Based Systems, pages 32–41. ISU TR #01-09.
Christensen, S. and Mortensen, K. H. (1996). Design/CPN ASK-CTL Manual. University of Aarhus.
de Almeida, H. O., da Silva, L. D., da Silva Oliveira, E., and Perkusich, A. (2005, to appear). A Formal Approach for Component Based Embedded Software Modelling and Analysis. In Proceedings of IEEE International Symposium on Industrial Electronics ISIE’05, Croatia.
Heineman, G. T., Crnkovic, I., Schmidt, H. W., Stafford, J. A., Szyperski, C. A., and Wallnau, K. C., editors (2005). Component-Based Software Engineering, 8th International Symposium, CBSE 2005, St. Louis, MO, USA, May 14-15, 2005, Proceedings, volume 3489 of Lecture Notes in Computer Science. Springer.
Jensen, K. (1997). Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, volume 2. Springer-Verlag.
Silva, L. D. and Perkusich, A. (2005). Composition of Software Artifacts Modelled Using Colored Petri Nets. Science of Computer Programming, 56(1):171–189.
Valmari, A. (1998). The State Explosion Problem. In Reisig, W. and Rozenberg, G., editors, Lectures on Petri Nets 1: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429–528. Springer-Verlag.
Almeida, H. O., Perkusich, A., Paes, R. B., and Costa, E. B. (2004b). Composição Dinâmica de Componentes para Aplicaç ões com Mudanças Frequëntes de Requisitos. In Anais do 4o Workshop de Desenvolvimento Baseado em Componentes, pages 9–14, João Pessoa, Paraıba, Brasil.
Aniorte, P. (2003). Componet-Based Software Development: From Component Model to Software Architecture. In ICSR7 2002 Workshop on Component-based Software Development Processes, Austin, Texas, USA.
Bernd Finkbeiner and Ingolf Kr¨uger (2001). Using Message Sequence Charts for Component-Based Formal Verification. In Giannakopoulou, D., Leavens, G. T., and Sitaraman, M., editors, SAVCBS 2001 Proceedings: Specification and Verification Component-Based Systems, pages 32–41. ISU TR #01-09.
Christensen, S. and Mortensen, K. H. (1996). Design/CPN ASK-CTL Manual. University of Aarhus.
de Almeida, H. O., da Silva, L. D., da Silva Oliveira, E., and Perkusich, A. (2005, to appear). A Formal Approach for Component Based Embedded Software Modelling and Analysis. In Proceedings of IEEE International Symposium on Industrial Electronics ISIE’05, Croatia.
Heineman, G. T., Crnkovic, I., Schmidt, H. W., Stafford, J. A., Szyperski, C. A., and Wallnau, K. C., editors (2005). Component-Based Software Engineering, 8th International Symposium, CBSE 2005, St. Louis, MO, USA, May 14-15, 2005, Proceedings, volume 3489 of Lecture Notes in Computer Science. Springer.
Jensen, K. (1997). Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, volume 2. Springer-Verlag.
Silva, L. D. and Perkusich, A. (2005). Composition of Software Artifacts Modelled Using Colored Petri Nets. Science of Computer Programming, 56(1):171–189.
Valmari, A. (1998). The State Explosion Problem. In Reisig, W. and Rozenberg, G., editors, Lectures on Petri Nets 1: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429–528. Springer-Verlag.
Published
2005-10-26
How to Cite
ALMEIDA, Hyggo; OLIVEIRA, Elthon; BARBOSA, Nádia; BUBLITZ, Frederico; DA SILVA, Leandro; PERKUSICH, Angelo.
Modeling and Formal Verification of Component-Based Information Systems. In: BRAZILIAN SYMPOSIUM ON INFORMATION SYSTEMS (SBSI), 2. , 2005, Florianópolis.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2005
.
p. 272-279.
DOI: https://doi.org/10.5753/sbsi.2005.14994.
