Lookup NU author(s): Luke Martin,
Professor Alexander Romanovsky
This is the authors' accepted manuscript of a conference proceedings (inc. abstract) that has been published in its final definitive form by Springer , 2016.
For re-use rights please refer to the publisher's terms and conditions.
This paper proposes a method in which to formally specify the design and reliability criteria of an advisory system for use within mission-critical contexts. This is motivated by increasing demands from industry to employ automated decision-support tools capable of operating as highly reliable applications under strict conditions. The proposed method applies the user requirements and design concept of the advisory system to define an abstract architecture. A Markov reliability model and real-time scheduling model are used to effectively capture the operational constraints of the system and are incorporated to the abstract architectural design to define an architectural model. These constraints describe component relationships, data flow and dependencies and execution deadlines of each component. This model is then expressed and proven using SPARK. It was found that the approach useful in simplifying the design process for reliable advisory systems, as well as effectively providing a good basis of a formal specification.
Author(s): Martin LJW, Romanovsky A
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: 8th International Workshop on Software Engineering for Resilient Systems (SERENE 2016)
Year of Conference: 2016
Online publication date: 26/08/2016
Acceptance date: 13/07/2016
Date deposited: 14/02/2018
Library holdings: Search Newcastle University Library for this item
Series Title: Lecture Notes in Computer Science