Um Enfoque Multiformalismos para Especificação de Sistemas de Segurança Crítica

  • Simone C. dos Santos UFPE
  • Fabio Q. B. da Silva UFPE

Resumo


Chamamos de sistemas de segurança crítica, aqueles sistemas cuja falha pode causar danos ao ambiente ou perigo de vida aos seres humanos ou ambos. Tais sistemas requerem um alto grau de confiabilidade em seu desenvolvimento, antes de serem colocados em uso. Este artigo descreve a utilização de métodos formais para aumentar a confiabilidade no desenvolvimento de sistemas de segurança crítica. O enfoque é inovador no sentido em que propõe a utilização de formalismos distintos para descrever aspectos diferentes do sistema e produz a integração das várias especificações através de provas de consistência. Os resultados descritos aqui fazem parte do trabalho desenvolvido em [4].

Referências

L. M. Barroca and J. A. McDermid. Formal methods: Use and relevance for the development of safety-critical systems. The Computer Journal vol 35(6), pages 579-599, 1992.

Glenn Bruns and Stuart Anderson. Using data consistency assumptions to show system safety, 1993. Laboratory for Foundations of Computer Science, Edinburgh.

Marcos Mota do Carmo Costa. Introdução à Lógica Modal Aplicada à Computação. Informática UFRGS, Departamento de Informática UFPE, 1992.

Simone C. dos Santos. Especificação formal no desenvolvimento de sistemas de segurança crítica (título preliminar). Dissertação de mestrado em andamento, Departamento de Informática, UFPE, 1995.

Narain Gehani and Andrew McGettrick. Software Specification Techniques. International Computer Science Series, N. J., 1986.

Farnam Jabanian and Aloysius Ka-Lau Mok. Safety analysis of timing properties in real-time. IEEE Transactions on Software Engineering, pages 890-901, 1986.

M. B. Josephs. A state-based approach to communicating processes. Distributed Computing, pages 9-18, 1988.

Ismar N. Kaufman. A aplicação de especificações formais no projeto lógico de software, 1992. Dissertação de Mestrado, Departamento de Informática, UFPE.

Leslie Lamport. The temporal logic of actions. Technical report, 1991. Digital Systems Research Center.

Nancy G. Leveson. Software safety: what, why and how. Computing Surveys vol 18(2), pages 125-163, 1986.

Nancy G. Leveson and Janice L. Stolay. Safety analysis using petri nets, IEEE Transactions on Software Engineering, pages 386-397, 1987.

A. Saced R. de Lemos and T. Anderson. A train as a case study for the requirements analysis of safety-critical systems. Computer Journal vol 35(1), pages 30-39, 1992.

Institute For Risk Research. Specification for a software program for a boiler water content monitor and control system, 1992. Waterloo, Canadá.

J. M. Spivey. The Z notation: A reference manual. Prentice-Hall, Englewood Cliffs NJ, 1989.

P. A. Lee T, Anderson and editors, Fault Tolerance: Principles and Practice. Prentice Hall, 1981.

J. B. Wordsworth. Software Development with Z. Addison-Wesley, England, 1992.
Publicado
03/10/1995
SANTOS, Simone C. dos; SILVA, Fabio Q. B. da. Um Enfoque Multiformalismos para Especificação de Sistemas de Segurança Crítica. In: SIMPÓSIO BRASILEIRO DE ENGENHARIA DE SOFTWARE (SBES), 9. , 1995, Recife/PE. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 1995 . p. 91-106. DOI: https://doi.org/10.5753/sbes.1995.24078.