Stochastic modelling Clause Samples
Stochastic modelling. There are relatively few tool-supported approaches for supporting the anal- ysis of stochastic models, and only limited experience in applying these to industry-scale problems. In WP2, Siemens has identified this as a priority in order to provide an analytic framework for discussing system-level failure rates on varying assumptions about specific component or infrastructure reli- abilities. Neither the Event-B language nor the Rodin tools currently support specification or analysis of probabilistic systems. Our initial work has focused on exploring the options for incorporating stochastic behaviour into Event-B models (Chapter 21). A case study inspired by the Siemens WP2 mini-pilot, on the behaviour of an emergency brake system in the presence of faults, has been a valuable focus point and forms the basis of a further study [And09] to be published shortly after the reporting period of this deliverable. This will compare Continuous Time Markov Chain approaches with proof-based techniques and lead to proposals for extensions to Event-B addressing this area. Part II Chapter 5 This chapter provides an overview of existing requirements engineering methods. Prior to any formal modelling, it is important to structure infor- mal requirements to ensure that the formal model realises what had been requested. Informal requirements documents typically present requirements in terms of disparate levels of abstraction and traceability to an Event-B model is rarely straightforward. We expect a suitable requirements engineering method to support trace- ability through the different abstraction levels of a refinement-based formal development. It should enable systematic validation of requirements through- out the development cycle.
5.1 provides an overview of current research that directly concerns the issues Deploy attempts to solve; Section 5.2 elaborates on the methods that have been used so far; Section 5.3 briefly lists the methods that we are aware of but haven’t considered pursuing at this point; we close with Section 5.4, where we outline our plans for the future.