University of Surrey

Test tubes in the lab Research in the ATI Dance Research

B annotations in critical control systems development.

Ifill, Wilson. (2008) B annotations in critical control systems development. Doctoral thesis, University of Surrey (United Kingdom)..

Full text is not currently available. Please contact sriopenaccess@surrey.ac.uk, should you require it.

Abstract

The design and implementation of critical controllers benefit from development in a formal method such as B. However, B does not support execution specification directly, which is a requirement in controller design. The aim here is to develop a set of annotations so that they can be used by a B design engineer to capture execution requirements, while creating the B model. The annotations, once shown to be machine-annotation consistent with the B machine, can be used independently from the machine to assess the correctness of CSP controllers developed to detail the control behaviour. CSP-B is a formal method integration that can be used to develop critical controller with both state and event behaviour. The advantages of using annotations is that the execution requirements can be captured and shown to be machine-annotation consistent during state operation development, and that a control loop invariant does not have to be independently developed. Handel-C is used on route to hardware synthesis as it supports the implementation of concurrency and the manipulation of state. Annotations are utilised again to guide the translation of the B and control annotations into Handel-C. This PhD. work has three main aims. Firstly, to introduce a set of annotations to describe control directives to permit controller development in B. The annotations capture execution requirements. They give rise to proof obligations that when discharged prove that the annotations are machine-annotation consistent with the machine they are written in, and therefore will not cause the machine to diverge. Secondly, we have proven that CSP controllers that are consistent with the annotations will preserve the non-divergence property established between the machine and the annotations. Thirdly, we show how annotation refinement is possible, and show a range of mappings from the annotated B and the consistent controller to Handel-C. The development of mappings demonstrates the feasibility of automatic translation of annotated B to Handel-C.

Item Type: Thesis (Doctoral)
Divisions : Theses
Authors :
NameEmailORCID
Ifill, Wilson.UNSPECIFIEDUNSPECIFIED
Date : 2008
Contributors :
ContributionNameEmailORCID
http://www.loc.gov/loc.terms/relators/THSUNSPECIFIEDUNSPECIFIEDUNSPECIFIED
Depositing User : EPrints Services
Date Deposited : 09 Nov 2017 12:12
Last Modified : 09 Nov 2017 14:40
URI: http://epubs.surrey.ac.uk/id/eprint/842966

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800