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

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

DOI: https://doi.org/10.5753/sbes.1995.24078

Abstract

Safety-critical systems are those systems whose fault may cause environmental damage or endanger human life. Such systems require a high degree of reliability in its development, before being put to normal use. This article describes the use of formal method to increase the reliability in the development of safety-critical systems. This approach is novel in the sense that it proposes the use of different formal methods to describe distinct aspects of the system and produces the integration of the various specifications via formal consistency profs. The results reported here are part of the work developed in [4].

References

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.