Formal Analysis of Real-time Requirements

Objectives:

To develop a method that can be practically used for analysing real-time software requirements resulting from the hazard scenarios represented by Fault Trees.

Contact:

The contact for this research project is here.

Rationale:

Safety analysis of systems comprising programmable components proved to be difficult both using traditional safety methods as well as software analysis techniques. A need for merging of these two approaches has been realised as to procure a methodology that would be able to analyse the computer component in the context of comprising system. The resulting technique would need to be adequately unequivocal, as to enable group work forced by complication of the systems as well as knowledge from various disciplines required to analyse them. On many of the systems described here more or less strict timing requirements are imposed, and analysis method for such systems would need to directly address this issue.

Safety analysis of computer control systems involves analyzing complex relations between system components, often including time relationships. The project explores how Fault Tree Analysis (FTA) can be extended in order to provide for analysis of time dependencies.

Approach:

One of possible analysis techniques to be utilised for examination of time-related computer-comprising safety-related system is to perform Fault-Tree Analysis augmented with formal semantics. The Fault Tree methodology is wide-spread and greatly appreciated in "classical" safety-related systems analysis.

Formalisation of a fault tree using Extended Common Safety Description Model (ECSDM) solves the problem of ambiguity of faults descriptions, as they are based here on system components states, as well as addresses the issue of timing aspects in a consistent way. The procedure consists of the following steps:

  • Creation of "traditional" fault tree,

  • Development of system model,

  • Description of faults in the tree using system component stated,

  • Description of timing relationships between faults,

  • Assessment of minimal cut sets and timing relationships between the sets elements.

If the method indicates there is a way wherein system could fail, the needed counter-measures can be deduced, and lack of such indication is a strong argument for system safety.

The method also defines an algorithm supporting deducing of safety time requirements for analysed system. The algorithm needs at its input the following data:

  • Results of minimal cut set and minimal cut set timing analysis,

  • Information timing of which events can be influenced by design decisions,

  • Timing restrictions of application domain.

Based on this data the algorithm proposes time restrictions to be imposed on influencable events to disable some (preferably all) of the ways system could fail. How and which of this restrictions (the resulting time restrictions can contain some alternatives) are to be implemented is a design decision.

Schedule:

  • The first phase of the project was in the period 1994-1997.

  • After the break the project was restarted in 2004.

  • In 2004 a tool supporting Timed Fault Tree Analysis was implemented.

  • In 2006 an algorithm supporting deducing of safety time requirements for analysed system was proposed.

  • It is planned to implement tool supporting requirements deduction and to seek for realistic industrial case studies in order to validate the approach.

Results:

At present the methodology includes defining of system faults in terms of its components states, provides a way of describing the timing relationships between events connected by a gate and an algorithm of deducing time relations between failures in minimal cut sets based on the relationships defined for each gate in a tree.

It also defines an algorithm for deducing timing requirements to be imposed on influencable events in order to make the analysed system safer.

The goal is to create tool support for the whole methodology and validate it using appropriate case studies.

PhD Thesis:

The results achieved till 1997 have been partially summarized in PhD thesis presented at the Gdansk University of Technology in 1997.

Andrzej Wardziński:
"ANALIZA DRZEW BŁĘDÓW SYSTEMÓW KOMPUTEROWYCH ZWIĄZANYCH Z BEZPIECZEŃSTWEM"
(The English title: "Analysis of Fault Trees for Safety Related Systems”)
Download PDF (2.7 MB)

Publications:

  1. Golaszewski G.: Czasowe wymagania bezpieczeństwa wobec systemu monitoringu ruchu drogowego, Proceedings of 5th National Conference on Information Technologies, Gdansk, Poland, 2007, pp. 265-272. (in Polish)

  2. Golaszewski G.: Dobór algorytmu do przetwarzania zależności czasowych w drzewach błędów, Proceedings of 14th Conference on Real-Time Systems, Karpacz, Poland, 2007, pp. 75-84. (in Polish)

  3. Golaszewski G., Gorski J.: Hazard prevention by forced time constraints, Proceedings of International Conference on Dependability of Computer Systems DepCoS–RELCOMEX’06, Szklarska Poręba, Poland, 25-27 May, 2006, IEEE Computer Society, pp. 84-91.

  4. Golaszewski G.: Automatyzacja określania wymagań bezpieczeństwa na podstawie wyników analizy czasowej drzew błędów, Proceedings of 4th National Conference on Information Technologies, vol. 11, Gdansk, Poland, 2006, pp. 631-638.

  5. Golaszewski G.: Tool support for ECSDM Fault Tree methodology, Proceedings of IEEE International Conference on Technologies for Homeland Security and Safety (TEHOSS 2005), Gdańsk, Poland, 2005, pp. 243-248.

  6. Golaszewski G., A system supporting the analysis of real-time requirements using Fault Trees, M.Sc. Thesis, Department of Software Engineering, Gdansk University of Technology, September 2004. (in Polish)

  7. Gorski J., Wardzinski A.: Timing Aspects of Safety Analysis, in: Safer Systems (F. Redmill and T. Anderson Eds.), Springer Verlag, 1997, pp. 231-244.

  8. Wardzinski A.: Fault Tree Analysis of Safety Related Computer Systems, PhD Thesis, Faculty of Electronics, Telecommunications and Informatics, Gdansk University of Technology, 1997. (in Polish)

  9. Gorski J., Wardzinski A.: Deriving Real-Time Requirements for Software from Safety Analysis, 8th EUROMICRO Workshop on Real-Time Systems, L'Aquila (Italy), June 12-14, 1996, IEEE Press, 1996, pp. 9-14.

  10. Gorski J., Wardzinski A.: Formalizing Fault Trees, in: Achievement and Assurance of Safety (F. Redmill and T. Anderson, eds.), Springer Verlag, 1995, pp. 311-327.

  11. Gorski J.: Extending Safety Analysis techniques with Formal Semantics, in: Technology and Assessment of Safety-Critical Systems (F.J. Redmill and T. Anderson, eds.), Springer-Verlag, 1994, pp. 147-163.

  12. Gorski J., Wardzinski A.: Formalizing Fault Trees, Safety Critical Systems Symposium, Brighton (UK), February 1995, Springer Verlag, 1994, pp. 311-327.

  13. Bloomfield R.E., Chang J.H., Gorski J.: Towards a Common Safety Description Model, Proceedings of Proceedings of 10th International Conference on Computer Safety, Reliability and Security (SAFECOMP'91), (J.F. Lindeberg, Ed.), Pergamon Press, 1991, pp. 1-6.

  14. Gorski J.: Towards a common formal semantics base for safety description model, EUREKA Project SEW 263, Report SDM/JG/01, 1990.

  15. Gorski J.: Interfacing fault trees to formal methods, EUREKA Project SEW 263, Report SDM/JG/03, 1990.
  16. Gorski J.: Deriving Safety Monitors from Formal Specifications, Proc. SAFECOMP'89, Vienna, Austria, Pergamon Press, 1989, pp. 123-128.
  17. Download PDF (431 kB)