Efficient and Mechanised Analysis of Infinite CSPz Specifications: strategy and tool support
Resumo
Verificação de modelos é uma técnica automática para verificar propriedades de sistemas com finitos estados. Para tratar sistemas com infinitos estados, que exibem o problema da explosão de estados, técnicas de compressão são usadas antes da verificação de modelos. Neste trabalho apresentamos uma maneira de analisar especificações CSPZ com infinitos estados baseada em abstração de dados. Implementamos também uma ferramenta de suporte que mecaniza o processo de abstração.Referências
Clarke, E., Grumberg, O. and Peled, D. (1999). Model Checking. The MIT Press.
Cousot, P. and Cousot, R. (1992). “Abstract interpretation frameworks”. J. Logic. and Comp., 2(4):511–547.
Farias, A. (2003). Efficient and Mechanised Analysis of Infinite CSPz Processes: strategy and tool support. Master’s dissertation, Federal University of Pernambuco.
Farias, A., Mota, A. and Sampaio, A. (2001). “De CSPz para CSPM: Uma ferramenta transformacional Java”. Workshop on Formal Methods (WMF’01), p. 1-10.
Farias, A., Mota, A. and Sampaio, A. (2003). “A Support Tool for CSPz Data Abstraction”. Tool Exhibition Notes of FME 2003, Pisa, Italy, 2003, p. 11-15.
Farias, A., Mota, A. and Sampaio, A. (2004). “Efficient CSPz Data Abstraction”. IFM 2004, volume 2999 of LNCS, p. 108-127.
Fischer, C. (2000). Combination and Implementation of Processes and Data: from CSPz to Java. PhD thesis, Fachbereich Informatik Universität Oldenburg.
Kesten, Y., Klein, A., Pnueli, A. and Raanan, G. (1999). “A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software”, volume 1708 of LNCS, p. 173-194.
Lazic, R. (1999). A semantic study of data-independence with applications to the mechanical verification of concurrent systems. PhD thesis, Oxford University.
Mota, A. (2001). Model Checking CSPz: Techniques to Overcome State Explosion. PhD thesis, Federal University of Pernambuco.
Mota, A. and Sampaio, A. (2001). “Model-Checking CSP-Z: Strategy, Tool Support and Industrial Application”. Science of Computer Programming, 40:59-96.
Mota, A., Borba, P. and Sampaio, A. (2002). “Mechanical Abstraction of CSPz Processes”. FME 2002, volume 2391 of LNCS, p. 163-183.
Roscoe, A. (1998). The Theory and Practice of Concurrency. Prentice Hall.
Saaltink, M. (1997). “The Z-Eves System”. ZUM’97: The Z Formal Specification Notation, volume 1212 of LNCS, Springer.
Spivey, M. (1992). The Z Notation: A Reference Manual. Prentice-Hall International.
Cousot, P. and Cousot, R. (1992). “Abstract interpretation frameworks”. J. Logic. and Comp., 2(4):511–547.
Farias, A. (2003). Efficient and Mechanised Analysis of Infinite CSPz Processes: strategy and tool support. Master’s dissertation, Federal University of Pernambuco.
Farias, A., Mota, A. and Sampaio, A. (2001). “De CSPz para CSPM: Uma ferramenta transformacional Java”. Workshop on Formal Methods (WMF’01), p. 1-10.
Farias, A., Mota, A. and Sampaio, A. (2003). “A Support Tool for CSPz Data Abstraction”. Tool Exhibition Notes of FME 2003, Pisa, Italy, 2003, p. 11-15.
Farias, A., Mota, A. and Sampaio, A. (2004). “Efficient CSPz Data Abstraction”. IFM 2004, volume 2999 of LNCS, p. 108-127.
Fischer, C. (2000). Combination and Implementation of Processes and Data: from CSPz to Java. PhD thesis, Fachbereich Informatik Universität Oldenburg.
Kesten, Y., Klein, A., Pnueli, A. and Raanan, G. (1999). “A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software”, volume 1708 of LNCS, p. 173-194.
Lazic, R. (1999). A semantic study of data-independence with applications to the mechanical verification of concurrent systems. PhD thesis, Oxford University.
Mota, A. (2001). Model Checking CSPz: Techniques to Overcome State Explosion. PhD thesis, Federal University of Pernambuco.
Mota, A. and Sampaio, A. (2001). “Model-Checking CSP-Z: Strategy, Tool Support and Industrial Application”. Science of Computer Programming, 40:59-96.
Mota, A., Borba, P. and Sampaio, A. (2002). “Mechanical Abstraction of CSPz Processes”. FME 2002, volume 2391 of LNCS, p. 163-183.
Roscoe, A. (1998). The Theory and Practice of Concurrency. Prentice Hall.
Saaltink, M. (1997). “The Z-Eves System”. ZUM’97: The Z Formal Specification Notation, volume 1212 of LNCS, Springer.
Spivey, M. (1992). The Z Notation: A Reference Manual. Prentice-Hall International.
Publicado
31/07/2004
Como Citar
FARIAS, Adalberto; MOTA, Alexandre; SAMPAIO, Augusto.
Efficient and Mechanised Analysis of Infinite CSPz Specifications: strategy and tool support. In: CONCURSO DE TESES E DISSERTAÇÕES (CTD), 17. , 2004, Salvador/BA.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2004
.
p. 64-68.
ISSN 2763-8820.
