{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T01:40:04Z","timestamp":1739929204598,"version":"3.37.3"},"reference-count":21,"publisher":"Wiley","issue":"8","license":[{"start":{"date-parts":[[2010,3,5]],"date-time":"2010-03-05T00:00:00Z","timestamp":1267747200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Concurrency and Computation"],"published-print":{"date-parts":[[2010,6,10]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The design and implementation of critical controllers benefit from development in a formal method such as the B\u2010Method. However, B does not support direct specification of executions, but this 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 consistent with the B machine, can be used independently to assess the correctness of the proposed CSP controllers. CSP||B is an alternative formal method integration that can be used to develop critical controllers with both state and event behaviour. The advantage of using annotations is that the execution requirements can be captured and shown to be consistent with the state during operation development, and that a control loop invariant to establish correctness does not have to be independently developed. Handel\u2010C is used on route to hardware synthesis as it supports the implementation of concurrency and the manipulation of state. Annotations are again used to guide the translation of the B and control annotations into Handel\u2010C. This work has three main aims. First, we 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 consistent with the machine they are written in, and therefore will not cause the machine to diverge. Second, we prove that CSP controllers that are consistent with the annotations will preserve the non\u2010divergence property established between the machine and the annotations. Third, we show how annotation refinement is possible, and show a range of mappings from annotated B and consistent controllers to Handel\u2010C. The development of mappings demonstrates the feasibility of automatic translation of annotated B to Handel\u2010C. Copyright \u00a9 2010 John Wiley &amp; Sons, Ltd.<\/jats:p>","DOI":"10.1002\/cpe.1427","type":"journal-article","created":{"date-parts":[[2010,3,5]],"date-time":"2010-03-05T08:39:02Z","timestamp":1267778342000},"page":"1023-1048","source":"Crossref","is-referenced-by-count":0,"title":["A step towards refining and translating B control annotations to Handel\u2010C"],"prefix":"10.1002","volume":"22","author":[{"given":"W.","family":"Ifill","sequence":"first","affiliation":[]},{"given":"S.","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2010,5,4]]},"reference":[{"key":"e_1_2_6_2_2","series-title":"Lecture Notes in Computer Science","first-page":"416","volume-title":"ZB2002: Formal Specification and Development in Z and B","author":"Treharne H","year":"2002"},{"key":"e_1_2_6_3_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162"},{"volume-title":"The B\u2010Method: An Introduction","year":"2001","author":"Schneider S","key":"e_1_2_6_4_2"},{"volume-title":"Communicating Sequential Processes","year":"1985","author":"Hoare CA","key":"e_1_2_6_5_2"},{"volume-title":"The Theory and Practice of Concurrency","year":"1998","author":"Roscoe AW","key":"e_1_2_6_6_2"},{"volume-title":"Concurrent and Real\u2010time Systems: The CSP Approach","year":"2000","author":"Schneider S","key":"e_1_2_6_7_2"},{"key":"e_1_2_6_8_2","series-title":"(Lecture Notes in Computer Science","first-page":"399","volume-title":"B2007: Formal Specification and Development in B","author":"Ifill W","year":"2007"},{"key":"e_1_2_6_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-1391-9_3"},{"volume-title":"The Designer's Guide to VHDL","year":"1996","author":"Ashenden PT","key":"e_1_2_6_10_2"},{"key":"e_1_2_6_11_2","unstructured":"IfillW.B annotations in critical control systems development. PhD Thesis Department of Computing University of Surrey 2008."},{"key":"e_1_2_6_12_2","unstructured":"IfillW.Formal development of an example processor (AEP) in AMN C and VHDL. MSc Thesis Royal Holloway University of London 1999."},{"key":"e_1_2_6_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSD.2003.1207723"},{"key":"e_1_2_6_14_2","doi-asserted-by":"crossref","unstructured":"AljerA DevienneP.Co\u2010design and refinement for safety critical systems. Nineteenth IEEE International Symposium on Defect and Fault Tolerance in VSLI Systems (DFT'04) Cannes France 2004;78\u201386.","DOI":"10.1109\/DFTVS.2004.1347827"},{"volume-title":"Event B Language","year":"2005","author":"Metayer C","key":"e_1_2_6_15_2"},{"key":"e_1_2_6_16_2","unstructured":"AbrialJ\u2010R.Event Driven Circuit Construction Version 5. MATISSE project 2001."},{"key":"e_1_2_6_17_2","unstructured":"TreharneH.Combining control executives and software specifications. PhD Thesis Royal Holloway University of London 2000."},{"key":"e_1_2_6_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(00)00023-X"},{"key":"e_1_2_6_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-35261-9_29"},{"key":"e_1_2_6_20_2","first-page":"399","volume-title":"Communicating Process Architectures 2007","author":"Ifill W","year":"2007"},{"volume-title":"Communicating Process Architectures 2004","year":"2004","author":"Phillips JD","key":"e_1_2_6_21_2"},{"key":"e_1_2_6_22_2","unstructured":"StepneyS.CSP\/FDR2 to Handel\u2010C translation. Technical Report University of York June2003."}],"container-title":["Concurrency and Computation: Practice and Experience"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fcpe.1427","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/cpe.1427","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T01:08:46Z","timestamp":1739927326000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/cpe.1427"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5,4]]},"references-count":21,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2010,6,10]]}},"alternative-id":["10.1002\/cpe.1427"],"URL":"https:\/\/doi.org\/10.1002\/cpe.1427","archive":["Portico"],"relation":{},"ISSN":["1532-0626","1532-0634"],"issn-type":[{"type":"print","value":"1532-0626"},{"type":"electronic","value":"1532-0634"}],"subject":[],"published":{"date-parts":[[2010,5,4]]}}}