[1] Jim Woodcock, Andy J. Wellings, and Ana Cavalcanti. Mobile CSP. In Márcio Cornélio and Bill Roscoe, editors, Formal Methods: Foundations and Applications---18th Brazilian Symposium, SBMF 2015, Belo Horizonte, Brazil, September 21--22, 2015, Proceedings, volume 9526 of Lecture Notes in Computer Science, pages 39--55. Springer, 2015. http://dx.doi.org/10.1007/978-3-319-29473-5_3. [ bib | DOI | .pdf ]
We describe an extension of imperative CSP with primitives to declare new event names and to exchange them by message passing between processes. We give examples in Mobile CSP to motivate the language design, and describe its semantic domain, based on the standard failures-divergences model for CSP, but also recording a dynamic event alphabet. The traces component is identical to the separation logic semantics of Hoare & O'Hearn. Our novel contribution is a semantics for mobile channels in CSP, described in Unifying Theories of Programming, that supports: compositionality with other language paradigms; channel faults, nondeterminism, deadlock, and livelock; multi-way synchronisation; and many-to-many channels. We compare and contrast our semantics with other approaches, including the pi-calculus, and consider implementation issues. As well as modelling reconfigurable systems, our extension to CSP provides semantics for techniques such as dynamic class-loading and the full use of dynamic dispatching and delegation.

[2] Ana Cavalcanti, Wen-ling Huang, Jan Peleska, and Jim Woodcock. CSP and Kripke structures. In Martin Leucker, Camilo Rueda, and Frank D. Valencia, editors, Theoretical Aspects of Computing---ICTAC 2015---12th International Colloquium Cali, Colombia, October 29--31, 2015, Proceedings, volume 9399 of Lecture Notes in Computer Science, pages 505--523. Springer, 2015. http://dx.doi.org/10.1007/978-3-319-25150-9_29. [ bib | DOI | .pdf ]
A runtime verification technique has been developed for CSP via translation of CSP models to Kripke structures. With this technique, we can check that a system under test satisfies properties of traces and refusals of its CSP model. This complements analysis facilities available for CSP and for all languages with a CSP-based semantics: Safety-Critical Java, Simulink, SysML, and so on. Soundness of the verification depends on the soundness of the translation and on the traceability of the Kripke structure analysis back to the CSP models and to the property specifications. Here, we present a formalisation of soundness by unifying the semantics of the languages involved: normalised graphs used in CSP model checking, action systems, and Kripke structures. Our contributions are the unified semantic framework and the formal argument itself.

Keywords: semantic models, UTP, formal testing, runtime verification
[3] John S. Fitzgerald, Carl Gamble, Peter Gorm Larsen, Kenneth Pierce, and Jim Woodcock. Cyber-physical systems design: Formal foundations, methods and integrated tool chains. In Stefania Gnesi and Nico Plat, editors, 3rd IEEE/ACM FME Workshop on Formal Methods in Software Engineering, FormaliSE 2015, Florence, Italy, May 18, 2015, pages 40--46. IEEE Computer Society, 2015. http://dx.doi.org/10.1109/FormaliSE.2015.14. [ bib | DOI | .pdf ]
The engineering of dependable cyber-physical systems (CPSs) is inherently collaborative, demanding cooperation between diverse disciplines. A goal of current research is the development of integrated tool chains for model-based CPS design that support co-modelling, analysis, co-simulation, testing and implementation. We discuss the role of formal methods in addressing three key aspects of this goal: providing reasoning support for semantically heterogeneous models, managing the complexity and scale of design space exploration, and supporting traceability and provenance in the CPS design set. We briefly outline an approach to the development of such a tool chain based on existing tools and discuss ongoing challenges and open research questions in this area.

[4] Sumesh Divakaran, Deepak D'Souza, Anirudh Kushwah, Prahladavaradan Sampath, Nigamanth Sridhar, and Jim Woodcock. Refinement-based verification of the FreeRTOS scheduler in VCC. In Michael Butler, Sylvain Conchon, and Fatiha Zaïdi, editors, Formal Methods and Software Engineering---17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3--5, 2015, Proceedings, volume 9407 of Lecture Notes in Computer Science, pages 170--186. Springer, 2015. http://dx.doi.org/10.1007/978-3-319-25423-4_11. [ bib | DOI | .pdf ]
We describe our experience with verifying the schedulerrelated functionality of FreeRTOS, a popular open-source embedded real-time operating system. We propose a methodology for carrying out refinement-based proofs of functional correctness of abstract data types in the popular code-level verifier VCC. We then apply this methodology to carry out a full machine-checked proof of the functional correctness of the FreeRTOS scheduler. We describe the bugs found during this exercise, the fixes made, and the effort involved.

[5] Simon Foster and Jim Woodcock. Mechanised theory engineering in Isabelle. In Maximilian Irlbeck, Doron A. Peled, and Alexander Pretschner, editors, Dependable Software Systems Engineering, volume 40 of NATO Science for Peace and Security Series, D: Information and Communication Security, pages 246--287. IOS Press, 2015. http://dx.doi.org/10.3233/978-1-61499-495-4-246. [ bib | DOI | .pdf ]
This is an introduction to mechanised theory engineering in Isabelle, an LCF-style interactive theorem prover. We introduce an embedding of Hoare & He's Unifying Theories of Programming (UTP) in Isabelle (named Isabelle/UTP) and show how to mechanise two key theories: relations and designs. These theories are su cient to give an account of the partial and total correctness of nondeterministic sequential programs and of networks of reactive processes. A tutorial introduction to each theory is interspersed with its formalisation and with mechanised proofs of relevant properties and theorems. The work described here underpins specification languages such as Circus, which combines state-rich imperative operations, communication and concurrency, object orientation, references and pointers, real time, and process mobility, all with denotational, axiomatic, algebraic, and operational semantics.

Keywords: Unifying Theories of Programming (UTP), denotational semantics, laws of programming, Isabelle, interactive theorem proving
[6] Alexandre Mota, Adalberto Farias, Jim Woodcock, and Peter Gorm Larsen. Model checking CML: tool development and industrial applications. Formal Asp. Comput., 27(5--6):975--1001, 2015. http://dx.doi.org/10.1007/s00165-015-0342-2. [ bib | DOI | .pdf ]
A model checker is an automatic tool that traverses the transition system (LTS) representation M of a given specification S (that belongs to a formal language L) to analyse the satisfaction of some (temporal) logical property f ; formally M |= f . In practice, however, model checkers are (in general) implementations of very optimised algorithms, aiming at achieving the best time and space complexities, without a clear association to the semantics of L. In this paper we show how to create a semantically guided model checker for L, given its operational semantics, following a hybrid semantics embedding. We use the framework FORMULA to this end and illustrate our strategy considering the formal language CML—a new language that was based on CSP, VDM and the refinement calculus proposed for modelling and analysis of systems of systems. As FORMULA is based on SMT solving, our model checker can handle infinite data communications and predicates by building and manipulating a symbolic LTS. This goes beyond the capabilities of traditional CSP model checkers such as FDR and PAT. Moreover, we show how to reduce time and space complexities by simple semantic modifications in the embedding. This allows a more semantics-preserving tuning. Finally, we show a real implementation of our model checker in an integrated development platform for CML and its practical use on industrial case studies.

Keywords: CML, model checker, analysis, FORMULA, operational semantics, SMT
[7] Shu Cheng, Jim Woodcock, and Deepak D'Souza. Using formal reasoning on a model of tasks for FreeRTOS. Formal Asp. Comput., 27(1):167--192, 2015. http://dx.doi.org/10.1007/s00165-014-0308-9. [ bib | DOI | .pdf ]
FreeRTOS is an open-source real-time microkernel that has a wide community of users. We present the formal specification of the behaviour of the task part of FreeRTOS that deals with the creation, management, and scheduling of tasks using priority-based preemption. Our model is written in the Z notation, and we verify its consistency using the Z/Eves theorem prover. This includes a precise statement of the preconditions for all API commands. This task model forms the basis for three dimensions of further work: (a) the modelling of the rest of the behaviour of queues, time, mutex, and interrupts in FreeRTOS; (b) refinement of the models to code to produce a verified implementation; and (c) extension of the behaviour of FreeRTOS to multi-core architectures. We propose all three dimensions as benchmark challenge problems for Hoare's Verified Software Initiative.

Keywords: Verified Software Initiative, FreeRTOS, formal verification, Z/Eves
[8] Claus Ballegaard Nielsen, Peter Gorm Larsen, John S. Fitzgerald, Jim Woodcock, and Jan Peleska. Systems of systems engineering: Basic concepts, model-based techniques, and research directions. ACM Comput. Surv., 48(2):18, 2015. http://doi.acm.org/10.1145/2794381. [ bib | DOI | .pdf ]
The term 'System of Systems' (SoS) has been used since the 1950s to describe systems that are composed of independent constituent systems, which act jointly towards a common goal through the synergism between them. Examples of SoS arise in areas such as power grid technology, transport, production and military enterprises. SoS engineering is challenged by the independence, heterogeneity, evolution and emergence properties found in SoS. This paper focuses on the role of model-based techniques within the SoS engineering field. A review of existing attempts to define and classify SoS is used to identify several dimensions that characterise SoS applications. The SoS field is exemplified by a series of representative systems selected from the literature on SoS applications. Within the area of model-based techniques the survey specifically reviews the state of the art for SoS modelling, architectural description, simulation, verification and testing. Finally, the identified dimensions of SoS characteristics are used to identify research challenges and future research areas of model-based SoS Engineering.

Keywords: system of systems, systems engineering, model-based engineering
[9] Kun Wei and Jim Woodcock. Towards algebraic semantics of Circus Time. In David Naumann, editor, Unifying Theories of Programming---5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers, volume 8963 of Lecture Notes in Computer Science, pages 84--104. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-14806-9_5. [ bib | DOI | .pdf ]
Over the years, the Circus family of notation has been used for specification, programming, and verification by refinement in many applications. Circus Time, a timed variant of Circus, plays a key role in dealing with timed behaviours. While most of the semantic developments of Circus Time have tended to focus on the denotational and operational sides, the work on its algebraic semantics is frustrated by the fact that the parallel operators are di cult to be reduced to other primitives in both discrete-time and continuous-time CSP models. In this paper, we present an algebraic operational semantics (AOS) of the discrete-time CSP in Circus Time. The related AOS form is identified in the timed context, and a complete set of algebraic laws are provided to transform any finite Circus Time programs into the AOS form. The AOS provides a solution to sequentialise the parallel operators and is also the major step towards a fully algebraic semantics.

Keywords: algebraic operational semantics, Circus Time, Timed CSP
[10] Simon Foster, Frank Zeyda, and Jim Woodcock. Isabelle/UTP: A mechanised theory engineering framework. In David Naumann, editor, Unifying Theories of Programming---5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers, volume 8963 of Lecture Notes in Computer Science, pages 21--41. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-14806-9_2. [ bib | DOI | .pdf ]
We introduce Isabelle/UTP, a novel mechanisation of Hoare and He's Unifying Theories of Programming (UTP) in Isabelle/HOL. UTP is a framework for the study, formalisation, and unification of formal semantics. Our contributions are, firstly, a deep semantic model of UTP's alphabetised predicates, supporting meta-logical reasoning that is parametric in the underlying notions of values and types. Secondly, integration of host-logic type checking that subsumes the need for typing proof obligations in the object-language. Thirdly, proof tactics that transfer results from well-supported mathematical structures in Isabelle to proofs about UTP theories. Additionally, our work provides novel insights towards reconciliation of shallow and deep language embeddings.

[11] Samuel Canham and Jim Woodcock. Three approaches to timed external choice in UTP. In David Naumann, editor, Unifying Theories of Programming---5th International Symposium, UTP 2014, Singapore, May 13, 2014, Revised Selected Papers, volume 8963 of Lecture Notes in Computer Science, pages 1--20. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-14806-9_1. [ bib | DOI | .pdf ]
We explore different approaches to modelling external choice as a reactive process in a UTP semantics with discrete time. The standard definition of external choice can not be simply reused in a timed semantics, since it can introduces behaviours which are not prefix-closed and urgent events which occur instantly. We first examine unstable states and urgent events in different semantics for CSP. We present the semantics for a simple timed reactive UTP language and describe the difficulties of adding external choice. We define two new process operators; strict choice, which never engages in urgent events and lazy choice, which can delay urgent events. We briefly discuss two potential modifications to the language model; a lazy semantics, in which termination is not unstable, and a semantics in which unstable states can be observed. Finally, we give a more detailed treatment to strict choice, expressing it as a reactive design and stating its algebraic laws.

[12] Simon Foster, Alvaro Miyazawa, Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, and Peter Gorm Larsen. An approach for managing semantic heterogeneity in systems of systems engineering. In 9th International Conference on System of Systems Engineering, SoSE 2014, Glenelg, Australia, June 9--13, 2014, pages 113--118. IEEE, 2014. http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6892473. [ bib | .pdf ]
Semantic heterogeneity is a significant challenge to integration in Systems of Systems Engineering (SoSE) due the large variety of languages, domains and tools which are used in their construction. In this paper we envision a strategy for managing this heterogeneity by decomposing domain specific languages into their “building block” theories which can be independently analysed, and used as a basis for linking with similar notations. This provides a systematic approach to building a tool-chain which integrates the different theories, methods and tools used in SoSE. Our approach has been piloted on the development of theories enabling machine-supported analysis of SysML models of SoSs. We conclude that the approach has further potential and identify lines of future research, notably in techniques for handling mixed discrete and continuous behaviour, timebands, mobility and model integration in SoSE.

Keywords: systems of systems, modelling, integration, unifying theories, tool-chain, theorem proving
[13] Alexandre Mota, Adalberto Farias, André Didier, and Jim Woodcock. Rapid prototyping of a semantically well founded Circus model checker. In Dimitra Giannakopoulou and Gwen Salaün, editors, Software Engineering and Formal Methods---12th International Conference, SEFM 2014, Grenoble, France, September 1--5, 2014. Proceedings, volume 8702 of Lecture Notes in Computer Science, pages 235--249. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-10431-7_17. [ bib | DOI | .pdf ]
Nowadays academia and industry use model checkers. These tools use search-based algorithms to check the satisfaction of some property f in M . Formally, M |= f , where M is a transition system representation of a specification written in a language L. Such a representation may come from the semantics of L. This paper presents a rapid prototyping of a model checker development strategy for Circus based on its operational semantics. We capture this semantics with the Microsoft FORMULA framework and use it to analyse (deadlock, livelock, and nondeterminism of) Circus specifications. As FORMULA supports SMT-solving, we can handle infinite data communications and predicates. Furthermore, we create a semantically well founded Circus model checker as long as executing FORMULA is equivalent to reasoning with First-Order Logic (Clark completion). We illustrate the use of the model-checker with an extract of an industrial case study.

Keywords: model checking, Circus, model-driven development, SMT
[14] Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, Simon Foster, and Peter Gorm Larsen. Contracts in CML. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications---6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8--11, 2014, Proceedings, Part II, volume 8803 of Lecture Notes in Computer Science, pages 54--73. Springer, 2014. http://dx.doi.org/10.1007/978-3-662-45231-8_5. [ bib | DOI | .pdf ]
We describe the COMPASS Modelling Language (CML), which is used to model large-scale Systems of Systems and the contracts that bind them together. The language can be used to document the interfaces to constituent systems using formal, precise, and verifiable specifications including preconditions, postconditions, and invariants. The semantics of CML directly supports the use of these contracts for all language constructs, including the use of communication channels, parallel processes, and processes that run forever. Every process construct in CML has an associated contract, allowing clients and suppliers to check that the implementations of constituent systems conform to their interface specifications.

[15] Jim Woodcock. Engineering UToPiA---Formal semantics for CML. In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods---19th International Symposium, Singapore, May 12--16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 22--41. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-06410-9_3. [ bib | DOI | .pdf ]
We describe the semantic domains for Compass Modelling Language (CML), using Hoare & He's Unifying Theories of Programming (UTP). CML has been designed to specify, design, compose, simulate, verify, test, and validate industrial systems of systems. CML is a semantically heterogeneous language, with state-rich imperative constructs based on VDM, communication and concurrency based on CSP, object orientation with object references, and discrete time based on Timed CSP. A key objective is to be semantically open, allowing further paradigms to be added, such as process mobility, continuous physical models, and stochastic processes. Our semantics deals separately with each paradigm, composing them with Galois connections, leading to a natural contract language for all constructs in all paradigms. The result is a compositional formal definition of a complex language, with the individual parts being available for reuse in other language definitions. The work backs our claim that use of UTP scales up to industrial-strength languages: Unifying Theories of Programming in Action (UToPiA).

[16] Pedro R. G. Antonino, Augusto Sampaio, and Jim Woodcock. A refinement based strategy for local deadlock analysis of networks of CSP processes. In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods---19th International Symposium, Singapore, May 12--16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 62--77. Springer, 2014. http://dx.doi.org/10.1007/978-3-319-06410-9_5. [ bib | DOI | .pdf ]
Based on a characterisation of process networks in the CSP process algebra, we formalise a set of behavioural restrictions used for local deadlock analysis. Also, we formalise two patterns, originally proposed by Roscoe, which avoid deadlocks in cyclic networks by performing only local analyses on components of the network; our formalisation systematises the behavioural and structural constraints imposed by the patterns. A distinguishing feature of our approach is the use of refinement expressions for capturing notions of pattern conformance, which can be mechanically checked by CSP tools like FDR. Moreover, three examples are introduced to demonstrate the effectiveness of our strategy, including a performance comparison between FDR default deadlock assertion and the verification of local behavioural constraints induced by our approach, also using FDR.

Keywords: local analysis, deadlock freedom, CSP, FDR, behavioural pattern
[17] James Mistry, Matthew Naylor, and Jim Woodcock. Adapting FreeRTOS for multicores: an experience report. Softw., Pract. Exper., 44(9):1129--1154, 2014. http://dx.doi.org/10.1002/spe.2188. [ bib | DOI | .pdf ]
Multicore processors are ubiquitous. Their use in embedded systems is growing rapidly and, given the constraints on uniprocessor clock speeds, their importance in meeting the demands of increasingly processor-intensive embedded applications cannot be understated. In order to harness this potential, system designers need to have available to them embedded operating systems with built-in multicore support for widely available embedded hardware. This paper documents our experience of adapting FreeRTOS, a popular embedded real-time operating system, to support multiple processors. A working multicore version of FreeRTOS is presented that is able to schedule tasks on multiple processors as well as provide full mutual exclusion support for use in concurrent applications. Mutual exclusion is achieved in an almost completely platform-agnostic manner, preserving one of FreeRTOS's most attractive features: portability.

Keywords: embedded systems, operating systems, multicore computing, task scheduling, software-based mutual exclusion, field-programmable gate-arrays
[18] Ana Cavalcanti, Steve King, Colin O'Halloran, and Jim Woodcock. Test-data generation for control coverage by proof. Formal Asp. Comput., 26(4):795--823, 2014. http://dx.doi.org/10.1007/s00165-013-0279-2. [ bib | DOI | .pdf ]
Many tools can check if a test set provides control coverage; they are, however, of little or no help when coverage is not achieved and the test set needs to be completed. In this paper, we describe how a formal characterisation of a coverage criterion can be used to generate test data; we present a procedure based on traditional programming techniques like normalisation, and weakest precondition calculation. It is a basis for automation using an algebraic theorem prover. In the worst situation, if automation fails to produce a specific test, we are left with a specification of the compliant test sets. Many approaches to model-based testing rely on formal models of a system under test. Our work, on the other hand, is not concerned with the use of abstract models for testing, but with coverage based on the text of programs. Although our examples present programs using a mathematical notation, they have a direct correspondence to code.

Keywords: control coverage, semantics, UTP, invariants
[19] Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors. Unifying Theories of Programming and Formal Engineering Methods - International Training School on Software Engineering, Held at ICTAC 2013, Shanghai, China, August 26--30, 2013, Advanced Lectures, volume 8050 of Lecture Notes in Computer Science. Springer, 2013. http://dx.doi.org/10.1007/978-3-642-39721-9. [ bib | DOI ]
This volume contains the lecture notes of the courses given at the ICTAC 2013 Software Engineering School on Unifying Theories of Programming and Formal Engineering Methods, held during August 26-30, 2013, in Shanghai. East China Normal University, UNU-IIST, and the University of York organized the school as part of the celebrations of the 70th birthday of He Jifeng. There were two associated events: Essays in Honor of He Jifeng on the Occasion of his 70th Birthday, Papers presented at a Symposium held in Shanghai during September 1--3, 2013; and Proceedings of the International Colloquium on Theoretical Aspects of Computing Held in Shanghai during September 4--6, 2013. The school is aimed at postgraduate students, researchers, academics, and industrial engineers who are interested in the state of the art in unifying theories of programming and formal engineering methods. This volume contains the lecture notes of the five courses. The common themes of the courses include the design and use of formal models and specification languages with tool support. System wide, the courses cover component-based and service-oriented systems, real-time systems, hybrid systems, and cyber physical systems. Techniques include inductive theorem proving, model checking, correct by construction through refinement and model transformations, synthesis and computer algebra. Two of the courses are explicitly related to Hoare and He's unifying theories. No previous knowledge of the topics involved is assumed.

[20] Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors. Theoretical Aspects of Computing---ICTAC 2013---10th International Colloquium, Shanghai, China, September 4--6, 2013. Proceedings, volume 8049 of Lecture Notes in Computer Science. Springer, 2013. http://dx.doi.org/10.1007/978-3-642-39718-9. [ bib | DOI ]
This volume contains the papers presented at ICTAC 2013: The 10th International Colloquium on Theoretical Aspects of Computing held during September 4-6, 2013, in Shanghai. There were 64 submissions and each was reviewed by at least three Program Committee members; the committee decided to accept 22 papers after thorough online discussions. The program also included three invited talks by Luca Cardelli, He Jifeng, and Marta Kwiatkowska. The conference was managed using the online system EasyChair. The International Colloquia on Theoretical Aspects of Computing (ICTAC) is a series of annual events funded in 2003 by the United Nations University International Institute for Software Technology (UNU-IIST). Its purpose is to bring together practitioners and researchers from academia, industry, and government to present research results and exchange experience and ideas. Beyond these scholarly goals, another main purpose is, as a mandate of the United Nations University, to promote cooperation in research and education between participants and their institutions from developing and industrial regions.

[21] Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors. Theories of Programming and Formal Methods---Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, volume 8051 of Lecture Notes in Computer Science. Springer, 2013. http://dx.doi.org/10.1007/978-3-642-39698-4. [ bib | DOI ]
Jifeng He is an outstanding computer scientist. He was born on August 5, 1943, in Shanghai, China. In his long academic career, he has made significant and wide-ranging contributions to the theories of programming and formal software engineering methods. To celebrate his 70th birthday, we present three LNCS volumes in his honor. Theories of Programming and Formal Methods, Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, Papers presented at a symposium held in Shanghai, September 1-3, 2013. Unifying Theories of Programming and Formal Engineering Methods, International Training School on Software Engineering, Shanghai, China, August 26-30, 2013. Theoretical Aspects of Computing---ICTAC 2013, 10th International Colloquium, Shanghai, China, September 4-6, 2013. He Jifeng is known for his seminal work in the theories of programming and formal methods for software engineering. He is particularly associated with Unifying Theories of Programming (UTP), the theory of data refinement and the laws of programming, and the rCOS formal method for object and component system construction. His book on UTP with Tony Hoare has been widely read and followed by a large number of researchers, and it has been used in many postgraduate courses. He was a senior researcher at Oxford during 1984-1998, and then a senior research fellow at the United Nations University International Institute for Software Technology (UNU-IIST) in Macau during 1998--2005. He has been a professor and is currently the Dean of the Institute of Software Engineering at East China Normal University, Shanghai, China. He was a founder of the International Conference of Formal Engineering Methods (ICEFM), the International Colloquium on Theoretical Aspects of Computing (ICTAC), and the International Symposium on Theoretical Aspects of Software Engineering (TASE). In 2005, He Jifeng was elected as an academician of the Chinese Academy of Sciences. He also received an honorary doctorate from the University of York. He has won a number of prestigious science and technology awards, including the second prize of the Natural Science Award from the State Council of China, the first prize of the Natural Science Award from the Ministry of Education of China, the first prize of Technology Innovation from the Ministry of Electronic Industry, and a number awards from Shanghai government.

[22] Marcel Vinicius Medeiros Oliveira, Ivan Soares de Medeiros Júnior, and Jim Woodcock. A verified protocol to implement multi-way synchronisation and interleaving in CSP. In Robert M. Hierons, Mercedes G. Merayo, and Mario Bravetti, editors, Software Engineering and Formal Methods---11th International Conference, SEFM 2013, Madrid, Spain, September 25--27, 2013. Proceedings, volume 8137 of Lecture Notes in Computer Science, pages 46--60. Springer, 2013. http://dx.doi.org/10.1007/978-3-642-40561-7_4. [ bib | DOI | .pdf ]
The complexity of concurrent systems can turn their development into a very complex and error-prone task. The use of formal methods like CSP considerably simplifies this task. Development, however, usually aims at reaching an executable program: a translation into a programming language is still needed and can be challenging. In previous work, we presented a tool, csp2hc, that translates a subset of CSP into Handel-C source code, which can itself be converted to produce files to program FPGAs. This subset restricts parallel composition: multisynchronisation and interleaving on shared channels are not allowed. In this paper, we present an extension to csp2hc that removes these restrictions. We provide a performance analysis of our code.

Keywords: concurrency, multi-synchronisation, compilation, protocols
[23] Victor Bandur and Jim Woodcock. Unifying theories of logic and specification. In Juliano Iyoda and Leonardo Mendonça de Moura, editors, Formal Methods: Foundations and Applications---16th Brazilian Symposium, SBMF 2013, Brasilia, Brazil, September 29--October 4, 2013, Proceedings, volume 8195 of Lecture Notes in Computer Science, pages 18--33. Springer, 2013. http://dx.doi.org/10.1007/978-3-642-41071-0_3. [ bib | DOI | http ]
We propose a unifying treatment of multi-valued logic in the general context of specification, presented in the style of the Unifying Theories of Programming of Hoare and He. At a low level, UTP theories correspond to different types of three-valued logic. At higher levels they correspond to individual specifications. Designs are considered as their models, but members of other unifying theories of computation can serve as models just as well. Using this setup we have the opportunity to show correspondences between specification languages that use different logics.

[24] Simon Foster and Jim Woodcock. Unifying theories of programming in Isabelle. In Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors, Unifying Theories of Programming and Formal Engineering Methods - International Training School on Software Engineering, Held at ICTAC 2013, Shanghai, China, August 26--30, 2013, Advanced Lectures, volume 8050 of Lecture Notes in Computer Science, pages 109--155. Springer, 2013. http://dx.doi.org/10.1007/978-3-642-39721-9_3. [ bib | DOI | .pdf ]
This is a tutorial introduction to the two most basic theories in Hoare & He's Unifying Theories of Programming and their mechanisation in the Isabelle interactive theorem prover. We describe the theories of relations and of designs (pre-postcondition pairs), interspersed with their formalisation in Isabelle and example mechanised proofs.

Keywords: Unifying Theories of Programming (UTP), denotational semantics, laws of programming, Isabelle, interactive theorem proving
[25] John S. Fitzgerald, Peter Gorm Larsen, and Jim Woodcock. Foundations for model-based engineering of systems of systems. In Marc Aiguier, Frédéric Boulanger, Daniel Krob, and Clotilde Marchal, editors, Complex Systems Design & Management, Proceedings of the Fourth International Conference on Complex Systems Design & Management CSD&M 2013, Paris, France, December 4--6, 2013, pages 1--19. Springer, 2013. http://dx.doi.org/10.1007/978-3-319-02812-5_1. [ bib | DOI | .pdf ]
The engineering of Systems of Systems presents daunting challenges. In this paper it is argued that rigorous semantic foundations for model-based techniques are potentially beneficial in addressing these. Three priorities for current research are identified: contractual interface definition, the verification of emergent behaviour, and the need to deal with semantic heterogeneity of constituent systems and their models. We describe the foundations of an approach in which architec- tural models in SysML may be analysed in a formal modelling language that has an extensible semantics given using the Unifying Theories of Programming (UTP).

[26] Ana Cavalcanti, Alexandre Mota, and Jim Woodcock. Simulink timed models for program verification. In Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors, Theories of Programming and Formal Methods---Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, volume 8051 of Lecture Notes in Computer Science, pages 82--99. Springer, 2013. http://dx.doi.org/10.1007/978-3-642-39698-4_6. [ bib | DOI | .pdf ]
Simulink is widely used by engineers to provide graphical specifications of control laws; its frequent use to specify safety-critical systems has motivated work on formal modelling and analysis of Simulink diagrams. The work that we present here is complementary: it targets verification of implementations by providing a refinement-based model. We use CircusTime, a timed version of the Circus notation that combines Z, CSP, and Morgan's refinement calculus with a time model, and which is firmly based on Hoare & He's Unifying Theories of Programming. We present a modelling approach that formalises the simulation time model that is routinely used for analysis. It is distinctive in that we use a refinement-based notation and capture functionality, concurrency, and time. The models produced in this way, however, are not useful for program verification, due to an idealised simulation time model; therefore, we describe how such models can be used to construct more realistic models. This novel modelling approach caters for assumptions about the programming environment, and clearly establishes

Keywords: Simulink, Z, CSP, Circus, time, refinement, modelling
[27] John S. Fitzgerald, Juan Bicarregui, Peter Gorm Larsen, and Jim Woodcock. Industrial deployment of formal methods: Trends and challenges. In Alexander Romanovsky and Martyn Thomas, editors, Industrial Deployment of System Engineering Methods, pages 123--143. Springer, 2013. http://dx.doi.org/10.1007/978-3-642-33170-1_10. [ bib | DOI | .pdf ]
The DEPLOY project has provided a rare opportunity to explore and document the potential benefits and challenges in creating and exploiting usable formal methods. Using the results of an updated review of 98 industrial applications, we identify trends relating to analytic power, robustness, stability and usability of tools, as well as the quality of evidence on costs and benefits of deployment. A consideration of the DEPLOY applications reinforces these trends, additionally emphasising the importance of selecting formalisms suited to the problem domain and of effectively managing traceable links between requirements and models.

[28] Ana Cavalcanti, Frank Zeyda, Andy J. Wellings, Jim Woodcock, and Kun Wei. Safety-Critical Java programs from Circus models. Real-Time Systems, 49(5):614--667, 2013. http://dx.doi.org/10.1007/s11241-013-9182-4. [ bib | DOI | .pdf ]
Safety-Critical Java (SCJ) is a novel version of Java that addresses issues related to real-time programming and certification of safety-critical applications. In this paper, we propose a technique that reveals the issues involved in the formal verification of an SCJ program, and provides guidelines for tackling them in a refinement-based approach. It is based on Circus, a combination of well established notations: Z, CSP, Timed CSP, and object orientation. We cater for the specification of timing requirements and their decomposition towards the structure of missions and event handlers of SCJ. We also consider the integrated refinement of value-based specifications into class-based designs using SCJ scoped memory areas. We present a refinement strategy, a Circus variant that captures the essence of the SCJ paradigm, and a substantial example based approach on a concurrent version of a case study that has been used as a benchmark by the SCJ community: an aircraft collision detector.

Keywords: SCJ, Circus, RTSJ, real-time systems, refinement, verification
[29] Kun Wei, Jim Woodcock, and Alan Burns. Modelling temporal behaviour in complex systems with timebands. Formal Methods in System Design, 43(3):520--551, 2013. http://dx.doi.org/10.1007/s10703-013-0193-5. [ bib | DOI | .pdf ]
Complex real-time systems exhibit dynamic behaviours on many different time levels. To cope with the wide range of time scales and produce more dependable computer-based systems, we develop a timebands model that can explicitly recognise a finite set of distinct time bands in which temporal properties and associated behaviours are described. We formalise the timebands model by using the semantics of TCSPM to guarantee soundness of each operator and maintain consistency and coordination between different time bands. By means of a complicated example, we demonstrate how significantly the timebands model contributes to describing complex real-time systems with multiple time scales.

[30] Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. Unifying theories in ProofPower-Z. Formal Asp. Comput., 25(1):133--158, 2013. http://dx.doi.org/10.1007/s00165-007-0044-5. [ bib | DOI | .pdf ]
The increasing interest in the combination of different computational paradigms is well represented by Hoare & He in the Unifying Theories of Programming (UTP). In this paper, we present a mechanisation of part of that work in a theorem prover, ProofPower-Z; the theories of alphabetised relations, designs, reactive and CSP processes are in the scope of this paper. Furthermore, the mechanisation of Circus, a language that combines Z, CSP, specification statements and Dijkstra's guarded command language, is also presented here. We also present an account of how this mechanisation is achieved, and more interestingly, of what issues were raised, and of our decisions. We aim at providing tool support not only for CSP and Circus, but also for further explorations of Hoare & He's unification, and for the mechanisation of languages whose semantics is based on the UTP.

Keywords: relational semantics, theorem proving, Circus.
[31] Ana Cavalcanti, Andy J. Wellings, and Jim Woodcock. The Safety-Critical Java memory model formalised. Formal Asp. Comput., 25(1):37--57, 2013. http://dx.doi.org/10.1007/s00165-012-0253-4. [ bib | DOI | .pdf ]
Safety-Critical Java (SCJ) is a version of Java for real-time programming, restricted to facilitate certification of implementations of safety-critical systems. Its development is the result of an international effort involving experts from industry and academia. What we provide here is, as far as we know, the first formalisation of the SCJ model of memory regions. We use Hoare and He's unifying theories of programming (UTP), enabling the integration of our theory with refinement models for object orientation and concurrency. In developing the SCJ theory, we also make a contribution to UTP by providing a general theory of invariants (an instance of which is used in the SCJ theory). The results presented here are a first essential ingredient to formalise the novel programming paradigm embedded in SCJ, and enable the justification and development of formal reasoning techniques based on refinement.

Keywords: Safety-Critical Java, memory safety, semantics, Unifying Theories of Programming, integration, refinement
[32] Jim Woodcock and Victor Bandur. Unifying theories of undefinedness in UTP. In Burkhart Wolff, Marie-Claude Gaudel, and Abderrahmane Feliachi, editors, Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27--28, 2012, Revised Selected Papers, volume 7681 of Lecture Notes in Computer Science, pages 1--22. Springer, 2012. http://dx.doi.org/10.1007/978-3-642-35705-3_1. [ bib | DOI | .pdf ]
In previous work, based on an original idea due to Saaltink, we proposed a unifying theory of undefined expressions in logics used for formally specifying software systems. In our current paper, we instantiate these ideas in Hoare and He's Unifying Theories of Programming, with each different treatment of undefinedness formalized as a UTP theory. In this setting, we show how to use classical logic to prove facts in a monotonic partial logic with guards, and we describe the guards for several different UTP theories. We show how classical logic can be used to prove semi-classical facts. We apply these ideas to the COMPASS Modelling Language (CML), which is an integration of VDM and CSP in the Circus tradition. We link CML, which uses McCarthy's left-to-right expression evaluation, and to VDM, which uses Jones's three-valued Logic of Partial Functions.

[33] Kun Wei, Jim Woodcock, and Ana Cavalcanti. Circus Time with reactive designs. In Burkhart Wolff, Marie-Claude Gaudel, and Abderrahmane Feliachi, editors, Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27--28, 2012, Revised Selected Papers, volume 7681 of Lecture Notes in Computer Science, pages 68--87. Springer, 2012. http://dx.doi.org/10.1007/978-3-642-35705-3_3. [ bib | DOI | .pdf ]
The UTP theories for CSP and Circus can be built by the combination of the theories of designs and reactive processes. Defining the CSP operators using reactive design provides a more concise, readable and uniform UTP semantics, and, more importantly, exposes the pre-postcondition semantics of the operators. For Circus Time, a few operators have been defined as reactive designs, but some important operators are still be considered. In this paper, we develop the reactive design semantics of sequential composition, hiding and recursion within Circus Time, and show how to prove some subtle laws using the new semantics.

Keywords: Circus Time, UTP, reactive designs
[34] Jim Woodcock, Ana Cavalcanti, John S. Fitzgerald, Peter Gorm Larsen, Alvaro Miyazawa, and S. Perry. Features of CML: A formal modelling language for systems of systems. In 7th International Conference on System of Systems Engineering, SoSE 2012, Genova, Italy, July 16--19, 2012, pages 445--450. IEEE, 2012. http://dx.doi.org/10.1109/SYSoSE.2012.6384144. [ bib | DOI | .pdf ]
We discuss the initial design for CML, the first formal language specifically designed for modelling and analysing Systems of Systems (SoSs). It is presented through the use of an example: an SoS of independent telephone exchanges. Its overall behaviour is first specified as a communicating process: a centralised telephone exchange. This description is then refined into a network of telephone exchanges, each handling a partition of the set of subscribers (telephone users). The refinement is motivated by a non-functional requirement to minimise the cabling required to connect geographically distributed subscribers, who are clustered. The exchanges remain as independent systems with respect to their local subscribers, whose service is unaffected by the loss of remote exchanges.

Keywords: architecture, SysML, modelling, specification, refinement, evolution, formal analysis, VDM, Circus, CML, semantics, UTP, enslavement pattern
[35] Alek Radjenovic, Richard F. Paige, Louis M. Rose, Jim Woodcock, and Steve King. A plug-in based approach for UML model simulation. In Antonio Vallecillo, Juha-Pekka Tolvanen, Ekkart Kindler, Harald Störrle, and Dimitrios S. Kolovos, editors, Modelling Foundations and Applications---8th European Conference, ECMFA 2012, Kgs. Lyngby, Denmark, July 2--5, 2012. Proceedings, volume 7349 of Lecture Notes in Computer Science, pages 328--339. Springer, 2012. http://dx.doi.org/10.1007/978-3-642-31491-9_25. [ bib | DOI | .pdf ]
Model simulation is a credible approach for model validation, complementary to others such as formal verification and testing. For UML 2.x, model simulations are available for state machines and communication diagrams; alternative finer-grained simulations, e.g., as are supported for Executable UML, are not available without significant effort (e.g., via profiles or model transformations). We present a flexible, plug-in based approach to enhance UML model simulation. We show how an existing simulation tool applicable to UML behavioural models can be extended to support external action language processors. The presented approach paves the way to enrich existing UML-based simulation tools with the ability to simulate external action languages.

[36] Kun Wei, Jim Woodcock, and Alan Burns. Modelling temporal behaviour in complex systems with timebands. In Mike Hinchey and Lorcan Coyle, editors, Conquering Complexity, pages 277--307. Springer, 2012. http://dx.doi.org/10.1007/978-1-4471-2297-5_13. [ bib | DOI | .pdf ]
Complex real-time systems exhibit dynamic behaviours on many different time levels. To cope with the wide range of time scales and produce more dependable computer-based systems, we develop a timebands model that can explicitly recognise a finite set of distinct time bands in which temporal properties and associated behaviours are described. We formalise the timebands model by using the semantics of TCSPM to guarantee soundness of each operator and maintain consistency and coordination between different time bands. By means of a complicated example, we demonstrate how significantly the timebands model contributes to describing complex real-time systems with multiple time scales.

[37] Juan Ignacio Perna and Jim Woodcock. Mechanised wire-wise verification of Handel-C synthesis. Sci. Comput. Program., 77(4):424--443, 2012. http://dx.doi.org/10.1016/j.scico.2010.02.007. [ bib | DOI | .pdf ]
The compilation of Handel-C programs into net-list descriptions of hardware components has been extensively used in commercial tools but never formally verified. In this paper we first introduce a variation of the existing semantic model for Handel-C compilation that is amenable for mechanical proofs and detailed enough to analyse properties about the generated hardware. We use this model to prove the correctness of the wiring schema used to interconnect the components at the hardware level and propagate control signals among them. Finally, we present the most interesting aspects of the mechanisation of the model and the correctness proofs in the HOL theorem prover.

[38] Ana Cavalcanti, Andy J. Wellings, Jim Woodcock, Kun Wei, and Frank Zeyda. Safety-Critical Java in Circus. In Andy J. Wellings and Anders P. Ravn, editors, The 9th International Workshop on Java Technologies for Real-time and Embedded Systems, JTRES '11, York, United Kingdom, September 26--28, 2011, pages 20--29. ACM, 2011. http://doi.acm.org/10.1145/2043910.2043915. [ bib | DOI | .pdf ]
This position paper proposes a refinement technique for the development of Safety-Critical Java (SCJ) programs. It is based on the Circus family of languages, which comprises constructs from Z, CSP, Timed CSP, and object-orientation. We cater for the specification of timing requirements, and their decomposition towards the structure of missions and event handlers of SCJ. We also consider the integrated refinement of value-based specifications into class-based designs using SCJ scoped memory areas. We present a refine- ment strategy, and a Circus variant that captures the essence of the SCJ paradigm independently from Java.

Keywords: verification
[39] Kun Wei, Jim Woodcock, and Alan Burns. Timed Circus: Timed CSP with the miracle. In Isabelle Perseil, Karin K. Breitman, and Roy Sterritt, editors, 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011, Las Vegas, Nevada, USA, 27--29 April 2011, pages 55--64. IEEE Computer Society, 2011. http://dx.doi.org/10.1109/ICECCS.2011.13. [ bib | DOI ]
Timed Circus is a compact extension to Circus; that is, it inherits only the CSP part of Circus while introducing time. Although it looks much like timed CSP from the viewpoint of syntax, its semantics is very different from that of timed CSP because it uses a complete lattice in the implication ordering instead of the complete partial order of the standard failures-divergences model of CSP. The complete lattice gives rise to a number of strange processes which violate some axioms of CSP, especially when the miracle (the top element) and SKIP meet time. In this paper, compared with timed CSP, we will extensively explore such strange processes which turn out to be very useful in specifying a distinct property that ‘something must occur'. Finally, we use a simple example to demonstrate how our model can contribute to modelling temporal behaviours with multiple time scales in complex systems.

[40] Osmar Marchi dos Santos, Jim Woodcock, and Richard F. Paige. Using model transformation to generate graphical counter-examples for the formal analysis of xUML models. In Isabelle Perseil, Karin K. Breitman, and Roy Sterritt, editors, 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011, Las Vegas, Nevada, USA, 27--29 April 2011, pages 117--126. IEEE Computer Society, 2011. http://dx.doi.org/10.1109/ICECCS.2011.19. [ bib | DOI ]
The INESS (INtegrated European Signalling System) Project, funded by the FP7 programme of the European Union, aims to provide a common, integrated, railway signalling system within Europe. INESS experts have been using the Executable UML (xUML) language to model an executable specification of the proposed system. Due to safety-critical aspects of these systems, one key idea is to formally analyse them. In this context, we have been working with other universities on different translation-based methods that enable the formal verification of xUML models. At the core of this approach is a verification framework based on model transformation technology, used to implement an automatic and transparent verification method for xUML. Since a translation-based approach is used, a key aspect to achieve transparency is the automatic generation of counter-examples for verified properties that have a false result during the analysis, in terms of the original xUML model. We describe in this paper how we achieve this using model transformation technology.

[41] Ana Cavalcanti, Andy J. Wellings, and Jim Woodcock. The Safety-Critical Java memory model: A formal account. In Michael J. Butler and Wolfram Schulte, editors, FM 2011: Formal Methods---17th International Symposium on Formal Methods, Limerick, Ireland, June 20--24, 2011. Proceedings, volume 6664 of Lecture Notes in Computer Science, pages 246--261. Springer, 2011. http://dx.doi.org/10.1007/978-3-642-21437-0_20. [ bib | DOI | .pdf ]
Safety-Critical Java (SCJ) is a version of Java for real-time programming that facilitates certification of implementations of safetycritical systems. It is the result of an international effort involving industry and academia. What we provide here is, as far as we know, the first formalisation of the SCJ model of memory regions. We use the Unifying Theories of Programming (UTP) to enable the integration of our theory with refinement models for object-orientation and concurrency. In developing the SCJ theory, we also make a contribution to the UTP by providing a general theory of invariants (of which the SCJ theory is an in- stance). Our results are a first essential ingredient to formalise the novel programming paradigm embedded in SCJ, and enable the justification and development of reasoning techniques based on refinement.

Keywords: semantics, UTP, integration, refinement
[42] Juan Ignacio Perna, Jim Woodcock, Augusto Sampaio, and Juliano Iyoda. Correct hardware synthesis---an algebraic approach. Acta Inf., 48(7--8):363--396, 2011. http://dx.doi.org/10.1007/s00236-011-0142-y. [ bib | DOI | .pdf ]
This paper presents an algebraic compilation approach to the correct synthesis (compilation into hardware) of a synchronous language with shared variables and parallelism. The synthesis process generates a hardware component that implements the source program by means of gradually reducing it into a highly parallel state-machine. The correctness of the compiler follows by construction from the correctness of the transformations involved in the synthesis process. Each transformation is proved sound from more basic algebraic laws of the source language; the laws are themselves formally derived from a denotational semantics expressed in the Unified Theories of Programming. The proposed approach is based on previous efforts that handle both software and hardware compilation, in a pure algebraic style, but the complexity of our source language demanded significant adaptations and extensions to the existing approaches.

Keywords: algebraic compilation, correct hardware synthesis
[43] Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, and Jim Woodcock, editors. Theoretical Aspects of Computing---ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1--3, 2010. Proceedings, volume 6255 of Lecture Notes in Computer Science. Springer, 2010. http://dx.doi.org/10.1007/978-3-642-14808-8. [ bib | DOI ]
The now well-established series of International Colloquia on Theoretical Aspects of Computing (ICTAC) brings together practitioners and researchers from academia, industry and government to present research results, and exchange experience and ideas. Beyond these scholarly goals, another main purpose is to promote cooperation in research and education between participants and their institutions, from developing and industrial countries. This volume contains the papers presented at ICTAC 2010. It was held during September 1-3 in the city of Natal, Rio Grande do Norte, Brazil. There were 68 submissions by authors from 24 countries all around the world. Each submission was reviewed by at least three, and on average four, Program Committee members and external reviewers. After extensive discussions, they decided to accept the 23 (regular) papers presented here. Authors of a selection of these papers were invited to submit an extended version of their work to a special issue of the Theoretical Computer Science journal. Seven of the papers were part of a special track including one paper on “Formal Aspects of Software Testing”, and six on the “Grand Challenge in Verified Software.” The special track was jointly organized by Marie-Claude Gaudel, from the Universit´e de Paris-Sud, and Jim Woodcock, from the University of York. The program also included invited talks. Ian Hayes, from the University of Queensland, Australia, was the FME lecturer. This volume includes his invited paper on a program algebra for sequential programs. We gratefully acknowledge the support of Formal Methods Europe in making the participation of Ian Hayes possible. A second invited paper is by Paulo Borba, from the Universidade Federal de Pernambuco, Brazil. His paper describes a refinement theory for software product lines. Stephan Merz, from INRIA, gave an invited talk on a proof assistant for TLA+; the abstract for his talk is also presented here. Wolfram Schulte, from Microsoft Research, gave a talk on verification of C programs.

[44] Jim Woodcock, Marcel Oliveira, Alan Burns, and Kun Wei. Modelling and implementing complex systems with timebands. In Fourth International Conference on Secure Software Integration and Reliability Improvement, SSIRI 2010, Singapore, June 9--11, 2010, pages 1--13. IEEE Computer Society, 2010. http://dx.doi.org/10.1109/SSIRI.2010.7. [ bib | DOI | .pdf ]
We describe how to use a timeband architecture to model real-time requirements. The architecture separates requirements that use different time units, producing a family of models. Each model is characterised by its granularity and precision. These models are then linked using superposition, a kind of event refinement, and a loose synchronisation of their time units, with respect to their precision. Our models are written using CSP and checked using the FDR model checker. More complicated models use Circus, the state-rich process algebra. We show how to implement such a timeband architecture using the JCSP Java class library.

Keywords: architecture, Circus, CSP, FDR, Java, JCSP, realtime systems, requirements modelling, event refinement, time granularity, timebands
[45] Kun Wei, Jim Woodcock, and Alan Burns. A timed model of Circus with the reactive design miracle. In José Luiz Fiadeiro, Stefania Gnesi, and Andrea Maggiolo-Schettini, editors, 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2010, Pisa, Italy, 13--18 September 2010, pages 315--319. IEEE Computer Society, 2010. http://dx.doi.org/10.1109/SEFM.2010.40. [ bib | DOI | .pdf ]
We propose a timed model of Circus which is a compact extension of original Circus. Apart from introducing time, this model uses UTP-style semantics to describe each process as a reactive design. One of significant contributions of our timed model is to extensively explore the reactive design miracle, the top element of a complete lattice with respect to the implication ordering. The employment of the miracle brings a number of brand-new features such as strong deadline and uninterrupted events, which provide a more powerful and flexible expressiveness in system specifications.

Keywords: Circus, UTP, Timed CSP, miracle
[46] Richard F. Paige, Jim Woodcock, Phillip J. Brooke, and Ana Cavalcanti. Programming phase: Formal methods. In Phillip A. Laplante, editor, Encyclopedia of Software Engineering, pages 772--785. Taylor & Francis, 2010. http://www.informaworld.com/10.1081/E-ESE-120044149. [ bib | .pdf ]
Formal methods involves the application of sound mathematical specification and reasoning techniques to the development of software systems. They can be applied across all phases of the engineering lifecycle. This chapter discusses their specific application to the programming phase, which can entail enrichment of executable code with mathematical artefacts (to support and improve our capabilities for reasoning), and the derivation of executable code from mathematical specifications. We provide an overview of some of the important approaches that can be applied to this phase.

[47] Brian Matthews, Arif Shaon, Juan Bicarregui, Catherine Jones, Esther Conway, and Jim Woodcock. Considering software preservation. ERCIM News, 2010(80), 2010. http://ercim-news.ercim.eu/en80/special/considering-software-preservation. [ bib | .pdf ]
Software is a class of electronic object which is by its very nature digital, and the preservation of software is often a vital prerequisite to the preservation of other electronic objects. However, software has many characteristics that make preserving it substantially more challenging than for many other types of digital object. Software is inherently complex, normally composed of a very large number of highly interdependent components and often forbiddingly opaque for people other than those who were directly involved in its development. Software is also highly sensitive to its operating environment, with the typical software artefact depending on a large number of other items including compilers, runtime environments, operating systems, documentation and even the hardware platform with its built-in software stack. Preserving a piece of software thus involves preserving much of its context as well.

[48] Marcel Vinicius Medeiros Oliveira and Jim Woodcock, editors. Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19--21, 2009, Revised Selected Papers, volume 5902 of Lecture Notes in Computer Science. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-10452-7. [ bib | DOI ]
This volume contains the papers presented at SBMF 2009: the Brazilian Symposium on Formal Methods, held during August 19--21, 2009 in Gramado, Rio Grande do Sul, Brazil. The SBMF programme included three invited talks given by Leonardo de Moura (Microsoft Research), Sebastian Uchitel (University of Buenos Aires and Imperial College London), and Daniel Kröning (University of Oxford).

[49] Andrew Butterfield, Pawel Gancarski, and Jim Woodcock. State visibility and communication in unifying theories of programming. In Wei-Ngan Chin and Shengchao Qin, editors, TASE 2009, Third IEEE International Symposium on Theoretical Aspects of Software Engineering, 29--31 July 2009, Tianjin, China, pages 47--54. IEEE Computer Society, 2009. http://dx.doi.org/10.1109/TASE.2009.57. [ bib | DOI | .pdf ]
We explore the interactions between programvariable state visibility and communication behaviour in state-rich CSP-like processes, using the Unifying Theories of Programming (UTP) framework. The key results of this work are: having variable state visible while a process is waiting to communicate, results in an operationally complex theory of behaviour; by contrast, considering state as unobservable during communication waitperiods results in an elegant theory, with much cleaner operational intuitions. The language constructs most affected by this observability choice are those of external choice and parallel composition. We also discuss situations where this state hiding can prevent the adoption of interesting operators that seize control from waiting processes.

[50] Emine G. Aydal, Richard F. Paige, Mark Utting, and Jim Woodcock. Putting formal specifications under the magnifying glass: Model-based testing for validation. In Second International Conference on Software Testing Verification and Validation, ICST 2009, Denver, Colorado, USA, April 1--4, 2009, pages 131--140. IEEE Computer Society, 2009. http://dx.doi.org/10.1109/ICST.2009.20. [ bib | DOI | .pdf ]
A software development process is effectively an abstract form of model transformation, starting from an end-user model of requirements, through to a system model for which code can be automatically generated. The success (or fail- ure) of such a transformation depends substantially on obtaining a correct, well-formed initial model that captures user concerns. Model-based testing automates black box testing based on the model of the system under analysis. This paper proposes and evaluates a novel model-based testing technique that aims to reveal specification/requirement-related errors by generating test cases from a test model and exercising them on the design model. The case study outlined in the paper presents that a separate test model not only increases the level of objectivity of the requirements, but also supports the validation of the system under test through test case generation. The results obtained from the case study supports the hypothesis that there may be discrepancies between the formal specification of the system modeled at developer end and the problem to be solved, and using solely formal verification methods may not be sufficient to reveal these. The approach presented in this paper aims at providing means to obtain greater confidence in the design model that is used as the basis for code generation.

[51] Osmar Marchi dos Santos, Jim Woodcock, Richard F. Paige, and Steve King. The use of model transformation in the INESS project. In Frank S. de Boer, Marcello M. Bonsangue, Stefan Hallerstede, and Michael Leuschel, editors, Formal Methods for Components and Objects---8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4--6, 2009. Revised Selected Papers, volume 6286 of Lecture Notes in Computer Science, pages 147--165. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-17071-3_8. [ bib | DOI ]
The INESS (INtegrated European Signalling System) Project, funded by the FP7 programme of the European Union, aims to provide a common, integrated, railway signalling system within Europe. INESS experts have been using the Executable UML (xUML) language to model an executable specification of the proposed system. Due to safetycritical aspects of these systems, one key idea is to formally analyse them. In this context, we have been working with other universities on different translation-based methods that enable the formal verification of xUML models. At the core of this approach is a verification framework based on model transformation technology, used to implement an automatic and transparent verification method for xUML. Since a translationbased approach is used, a key aspect to achieve transparency is the automatic generation of counter-examples for verified properties that have a false result during the analysis, in terms of the original xUML model. We describe in this paper how we achieve this using model transformation technology.

Keywords: model transformation, executable UML, formal verification
[52] Juan Bicarregui, John S. Fitzgerald, Peter Gorm Larsen, and J. C. P. Woodcock. Industrial practice in formal methods: A review. In Ana Cavalcanti and Dennis Dams, editors, FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2--6, 2009. Proceedings, volume 5850 of Lecture Notes in Computer Science, pages 810--813. Springer, 2009. http://dx.doi.org/10.1007/978-3-642-05089-3_52. [ bib | DOI | .pdf ]
We examine the the industrial application of formal methods using data gathered in a review of 62 projects taking place over the last 25 years. The review suggests that formal methods are being applied in a wide range of application domains, with increasingly strong tool support. Significant challenges remain in providing usable tools that can be integrated into established development processes; in education and training; in taking formal methods from first use to second use, and in gathering and evidence to support informed selection of methods and tools.

[53] Jean-Raymond Abrial, Michael J. Butler, Rajev Joshi, Elena Troubitsyna, and J. C. P. Woodcock. 09381 extended abstracts collection---refinement based methods for the construction of dependable systems. In Jean-Raymond Abrial, Michael J. Butler, Rajev Joshi, Elena Troubitsyna, and J. C. P. Woodcock, editors, Refinement Based Methods for the Construction of Dependable Systems, 13.09.--18.09.2009, volume 09381 of Dagstuhl Seminar Proceedings. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, Germany, 2009. http://drops.dagstuhl.de/opus/volltexte/2010/2374/. [ bib ]
With our growing reliance on computers, the total societal costs of their failures are hard to underestimate. Nowadays computers control critical systems from various domains such as aerospace, automotive, railway, business etc. Obviously, such systems must have a high degree of dependability---a degree of trust that can be justifiably placed on them. Although the currently operating systems do have an acceptable level of dependability, we believe that they development process is still rather immature and ad-hoc. The constantly growing system complexity poses an increasing challenge on the system developers and requires significant improvement on the existing developing practice. To address this problem, we investigated how to establish a set of refinement-based engineering methods that can provide the designers with a systematic methodology for development of complex systems.

[54] Leo Freitas, Jim Woodcock, and Yichi Zhang. Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository. Sci. Comput. Program., 74(4):197--218, 2009. http://dx.doi.org/10.1016/j.scico.2008.09.012. [ bib | DOI | .pdf ]
Parts of the CICS transaction processing system were modelled formally in the 1980s in a collaborative project between IBM Hursley Park and Oxford University Computing Laboratory. Z was used to capture a precise description of the behaviour of various modules as a means of communicating requirements and design intentions. These descriptions were not mechanically verified in any way: proof tools for Z were not considered mature, and no business case was made for effort in this area. We report a recent experiment on using the Z/Eves mechanical theorem prover to construct a machine-checked analysis of one of the CICS modules: the File Control API. This work was carried out as part of the international Grand Challenge in Verified Software, and our results are recorded in the Verified Software Repository. We give a brief description of the other modules, and propose them as challenge problems for the verification community.

[55] Leo Freitas, Jim Woodcock, and Zheng Fu. POSIX file store in Z/Eves: An experiment in the verified software repository. Sci. Comput. Program., 74(4):238--257, 2009. http://dx.doi.org/10.1016/j.scico.2008.08.001. [ bib | DOI | .pdf ]
We present results from the second pilot project in the international Verification Grand Challenge: a formally verified specification of a POSIX-compliant file store using the Z/Eves theorem prover. The project's overall objective is to build a verified file store for space-flight missions. Our specification of the file store is based on Morgan & Sufrin's specification of the UNIX filing system; the proof and its mechanisation in Z/Eves are novel. We show how our work contributes towards building a verified software repository: a set of general theories and experiments reusable across different domains.

[56] Andrew Butterfield, Leo Freitas, and Jim Woodcock. Mechanising a formal model of flash memory. Sci. Comput. Program., 74(4):219--237, 2009. http://dx.doi.org/10.1016/j.scico.2008.09.014. [ bib | DOI | .pdf ]
We present second steps in the construction of formal models of NAND flash memory, based on a recently emerged open standard for such devices. The model is intended as a key part of a pilot project to develop a verified file store system based on flash memory. The project was proposed by Joshi and Holzmann as a contribution to the Grand Challenge in Verified Software, and involves constructing a highly assured flash file store for use in space-flight missions. The model is at a level of abstraction that captures the internal architecture of NAND flash devices. In this paper, we focus on mechanising the state model and its initialisation operation, where most of the conceptual complexity resides

Keywords: grand challenge, verification, flash hardware, theorem proving
[57] Leo Freitas and Jim Woodcock. A chain datatype in Z. Int. J. Software and Informatics, 3(2--3):357--374, 2009. http://www.ijsi.org/ch/reader/view_abstract.aspx?file_no=357&flag=1. [ bib | .pdf ]
We present results about a general-purpose chain datatype spec- ified in the Z notation and mechanised using the Z/Eves theorem prover. Our particular interest comes from its use in the specification and refinement of operating system kernels for embedded real-time devices as part of a pilot project within the international Grand Chal- lenge in Verified Software, and to contribute to the Verified Software Repository. We show---at a fairly high level---the sort of dogged work that is needed to get a body of results together to form a basis for future projects. Our work discusses important hidden and missing properties in the specification of the chain datatype and its relation to kernel design.

[58] Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. A UTP semantics for Circus. Formal Asp. Comput., 21(1--2):3--32, 2009. http://dx.doi.org/10.1007/s00165-007-0052-5. [ bib | DOI | .pdf ]
Circus specifications define both data and behavioural aspects of systems using a combination of Z and CSP constructs. Previously, a denotational semantics has been given to Circus; however, a shallow embedding of Circus in Z, in which the mapping from Circus constructs to their semantic representation as a Z specification, with yet another language being used as a meta-language, was not useful for proving properties like the refinement laws that justify the distinguishing development technique associated with Circus. This work presents a final reference for the Circus denotational semantics based on Hoare and He's Unifying Theories of Programming (UTP); as such, it allows the proof of meta-theorems about Circus including the refinement laws in which we are interested. Its correspondence with the CSP semantics is illustrated with some examples. We also discuss the library of lemmas and theorems used in the proofs of the refinement laws. Finally, we give an account of the mechanisation of the Circus semantics and of the mechanical proofs of the refinement laws.

Keywords: relational model, concurrency, refinement calculus, theorem proving
[59] Leo Freitas and Jim Woodcock. FDR explorer. Formal Asp. Comput., 21(1--2):133--154, 2009. http://dx.doi.org/10.1007/s00165-008-0074-7. [ bib | DOI | .pdf ]
In this paper we describe the internal structures of FDR, the refinement model checker for Hoare's Communicating Sequential Processes (CSP), as well as an Application Programming Interface (API) allowing one to interact more closely with, and have fine grained control over, FDR's behaviour and data structures. FDR stands for Failures Divergences Refinement. With such information it is possible to create optimised CSP code to perform refinement checks that are more space/time efficient, hence enabling the analysis of more complex and data intensive specifications. This information is very valuable for both CSP users and tools that automatically generate CSP code, such as those related to security analysis generating test-cases as CSP processes. We present examples of using the tool, which include advanced features like FDR's transparent functions that can be used to considerably compress the state space to be checked. Finally, we show how one can transform FDR's graph format into a graph notation (e.g., JGraph), hence enabling visualisation of Labelled Transition Systems (LTS) of CSP specifications.

Keywords: refinement, model checking, CSP, FDR, Labelled Transition Systems, automata
[60] Juan Ignacio Perna and Jim Woodcock. Mechanised wire-wise verification of Handel-C synthesis. Electr. Notes Theor. Comput. Sci., 240:201--219, 2009. http://dx.doi.org/10.1016/j.entcs.2009.05.053. [ bib | DOI | .pdf ]
The compilation of Handel-C programs into net-list descriptions of hardware components has been extensively used in commercial tools but never formally verified. In this paper we first introduce a variation of the existing semantic model for Handel-C compilation that is amenable for mechanical proofs and detailed enough to analyse properties about the generated hardware. We use this model to prove the correctness of the wiring schema used to interconnect the components at the hardware level and propagate control signals among them. Finally, we present the most interesting aspects of the mechanisation of the model and the correctness proofs in the HOL theorem prover.

[61] Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John S. Fitzgerald. Formal methods: Practice and experience. ACM Comput. Surv., 41(4), 2009. http://doi.acm.org/10.1145/1592434.1592436. [ bib | DOI | .pdf ]
Formal methods use mathematical models for analysis and verification at any part of the program life-cycle. We describe the state of the art in the industrial use of formal methods, concentrating on their increasing use at the earlier stages of specification and design. We do this by reporting on a new survey of industrial use, comparing the situation in 2009 with the most significant surveys carried out over the last 20 years. We describe some of the highlights of our survey by presenting a series of industrial projects, and we draw some observations from these surveys and records of experience. Based on this, we discuss the issues surrounding the industrial adoption of formal methods. Finally, we look to the future and describe the development of a Verified Software Repository, part of the worldwide Verified Software Initiative. We introduce the initial projects being used to populate the repository, and describe the challenges they address.

Keywords: experimental software engineering, formal methods surveys, grand challenges, Verified Software Initiative, Verified Software Repository
[62] Natarajan Shankar and Jim Woodcock, editors. Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6--9, 2008. Proceedings, volume 5295 of Lecture Notes in Computer Science. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-87873-5. [ bib | DOI ]
This volume contains the papers presented at the Second Working Conference on Verified Software: Theories, Tools, and Experiments held in Toronto during October 6–9, 2008. This followed a successful working conference held in Zurich in 2005, also published in Lecture Notes in Computer Science as volume 4171. The second conference formally inaugurated the Verified Software Initiative (VSI), a 15-year, co-operative, international project directed at the scientific challenges of large-scale software verification. The scope of the cooperative effort includes the sharing and interoperability of tools, the alignment of theory and practice, the identification of challenge problems, the construction of benchmark suites, and the execution of large-scale experiments. The conference was open to everyone interested in participating actively in the VSI effort.

[63] Jim Woodcock. The miracle of reactive programming. In Andrew Butterfield, editor, Unifying Theories of Programming, Second International Symposium, UTP 2008, Dublin, Ireland, September 8--10, 2008, Revised Selected Papers, volume 5713 of Lecture Notes in Computer Science, pages 202--217. Springer, 2008. http://dx.doi.org/10.1007/978-3-642-14521-6_12. [ bib | DOI | .pdf ]
Reactive miracles are rather unexplored in Unifying Theories of Programming. We present two simple properties: prefixing a miracle with an event, and offering an external choice between a process and a miracle. Both are strange processes, each violating an important axiom of the standard failures-divergences model for CSP.

[64] Juan Ignacio Perna and Jim Woodcock. UTP semantics for Handel-C. In Andrew Butterfield, editor, Unifying Theories of Programming, Second International Symposium, UTP 2008, Dublin, Ireland, September 8--10, 2008, Revised Selected Papers, volume 5713 of Lecture Notes in Computer Science, pages 142--160. Springer, 2008. http://dx.doi.org/10.1007/978-3-642-14521-6_9. [ bib | DOI ]
Only limited progress has been made so far towards an axiomatic semantics or discovering the algebraic rules that characterise Handel-C programs. In this paper we present a UTP semantics together with extensions we needed to include in order to express Handel-C properties that were not addressable with standard UTP. We also show how our extensions can be abstracted to a more general context and prove a set of algebraic rules that hold for them. Finally, we use the semantics to prove some properties about Handel-C constructs.

[65] Alistair A. McEwan and Jim Woodcock. Unifying theories of interrupts. In Andrew Butterfield, editor, Unifying Theories of Programming, Second International Symposium, UTP 2008, Dublin, Ireland, September 8--10, 2008, Revised Selected Papers, volume 5713 of Lecture Notes in Computer Science, pages 122--141. Springer, 2008. http://dx.doi.org/10.1007/978-3-642-14521-6_8. [ bib | DOI | .pdf ]
The concept of an interrupt is one that appears across many paradigms, and used in many different areas. It may be used as a device to assist specifications to model failure, or to describe complex interactions between non co-operating components. It is frequently used in hardware to allow complex scheduling patterns. Although interrupts are ubiquitous in usage, the precise behaviour of a system incorporating interrupts can be difficult to reason about and predict. In this paper, a complete theory of the interrupt operator presented by Hoare in his original treatment of CSP is proposed. The semantics are given in the CSP model in Unifying Theories of Programming. New and existing algebraic laws are proposed and justified. The contribution of the paper is therefore a denotational semantics of an interrupt operator, and a collection of algebraic laws that assist in reasoning about systems incorporating interrupts.

[66] Emine G. Aydal, Mark Utting, and Jim Woodcock. A comparison of state-based modelling tools for model validation. In Richard F. Paige and Bertrand Meyer, editors, Objects, Components, Models and Patterns, 46th International Conference, TOOLS EUROPE 2008, Zurich, Switzerland, June 30--July 4, 2008. Proceedings, volume 11 of Lecture Notes in Business Information Processing, pages 278--296. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-69824-1_16. [ bib | DOI | .pdf ]
In model-based testing, one of the biggest decisions taken before modelling is the modelling language and the model analysis tool to be used to model the system under investigation. UML, Alloy and Z are examples of popular state-based modelling languages. In the literature, there has been research about the similarities and the differences between modelling languages. However, we believe that, in addition to recognising the expressive power of modelling languages, it is crucial to detect the capabilities and the weaknesses of analysis tools that parse and analyse models written in these languages. In order to explore this area, we have chosen four model analysis tools: USE, Alloy Analyzer, ZLive and ProZ and observed how modelling and validation stages of MBT are handled by these tools for the same system. Through this experiment, we not only concretise the tasks that form the modelling and validation stages of MBT process, but also reveal how efficiently these tasks are carried out in different tools.

[67] Will Harwood, Ana Cavalcanti, and Jim Woodcock. A theory of pointers for the UTP. In John S. Fitzgerald, Anne Elisabeth Haxthausen, and Hüsnü Yenigün, editors, Theoretical Aspects of Computing---ICTAC 2008, 5th International Colloquium, Istanbul, Turkey, September 1--3, 2008. Proceedings, volume 5160 of Lecture Notes in Computer Science, pages 141--155. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-85762-4_10. [ bib | DOI | .pdf ]
Hoare and He's unifying theories of programming (UTP) provide a collection of relational models that can be used to study and compare several programming paradigms. In this paper, we add to the UTP a theory of pointers and records that provides a model for objects and sharing in languages like Java and C++. Our work is based on the hierarchical addressing scheme used to refer to record fields (or object attributes) in conventional languages, rather than explicit notions of location. More importantly, we support reasoning about the structure and sharing of data, as well as their, possibly infinite, values. We also provide a general account of UTP theories characterised by conjunctive healthiness conditions, of which our theory is an example.

Keywords: semantics, refinement, relations, object models
[68] Emine G. Aydal, Richard F. Paige, and Jim Woodcock. Observations for assertion-based scenarios in the context of model validation and extension to test case generation. In First International Conference on Software Testing Verification and Validation, ICST 2008, Lillehammer, Norway, April 9--11, 2008, Workshops Proceedings, pages 11--20. IEEE Computer Society, 2008. http://dx.doi.org/10.1109/ICSTW.2008.29. [ bib | DOI | .pdf ]
Some approaches to Model-Based Testing focus on test case generation from assertions (operation pre- and postconditions) and invariants, e.g., written in the Object Constraint Language. In such a setting, assertions must be validated. Validation is often carried out via executing scenarios wherein system operations are applied, to detect unsatisfied invariants or failed preconditions. This paper aims to improve the understanding of how to write useful validation scenarios for assertions in OCL. To do so, we report on our experiences during the creation and execution of 237 scenarios for validating assertions for the Mondex Smart Card application, and describe several observations that can help to improve the process of writing these scenarios. We also describe the important factors that must be considered in transforming these scenarios into abstract test cases.

[69] Jim Woodcock and Leo Freitas. Linking VDM and Z. In 13th International Conference on Engineering of Complex Computer Systems (ICECCS 2008), March 31 2008--April 3 2008, Belfast, Northern Ireland, pages 143--152. IEEE Computer Society, 2008. http://dx.doi.org/10.1109/ICECCS.2008.36. [ bib | DOI | .pdf ]
The International Grand Challenge in Verified Software is benchmarking current verification technology by con- ducting a series of experiments, and one such experiment is to build a verified POSIX-compliant flash filestore. An objective of this experiment is to combine different formal methods, and this raises issues about the different logics used. One significant area of difference is in the treatment of undefined expressions, and we show how this difference can be overcome using a unifying theory. This then allows us to use a theorem prover for Z to verify theorems about a data type specified and refined in VDM.

[70] Leo Freitas, Jim Woodcock, and Andrew Butterfield. POSIX and the verification grand challenge: A roadmap. In 13th International Conference on Engineering of Complex Computer Systems (ICECCS 2008), March 31 2008--April 3 2008, Belfast, Northern Ireland, pages 153--162. IEEE Computer Society, 2008. http://dx.doi.org/10.1109/ICECCS.2008.35. [ bib | DOI ]
[71] Jim Woodcock and Paul Boca. ABZ2008 VSR-Net workshop. In Egon Börger, Michael J. Butler, Jonathan P. Bowen, and Paul Boca, editors, Abstract State Machines, B and Z, First International Conference, ABZ 2008, London, UK, September 16--18, 2008. Proceedings, volume 5238 of Lecture Notes in Computer Science, pages 378--379. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-87603-8_48. [ bib | DOI ]
[72] Jim Woodcock, Susan Stepney, David Cooper, John A. Clark, and Jeremy Jacob. The certification of the Mondex electronic purse to ITSEC level E6. Formal Asp. Comput., 20(1):5--19, 2008. http://dx.doi.org/10.1007/s00165-007-0060-5. [ bib | DOI ]
[73] Leo Freitas and Jim Woodcock. Mechanising Mondex with Z/Eves. Formal Asp. Comput., 20(1):117--139, 2008. http://dx.doi.org/10.1007/s00165-007-0059-y. [ bib | DOI ]
[74] Emine G. Aydal, Richard F. Paige, and Jim Woodcock. Evaluation of OCL for large-scale modelling: A different view of the Mondex purse. ECEASST, 9, 2008. http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/102. [ bib ]
[75] Paulo Borba, Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock, editors. Testing Techniques in Software Engineering, Second Pernambuco Summer School on Software Engineering, PSSE 2007, Recife, Brazil, December 3--7, 2007, Revised Lectures, volume 6153 of Lecture Notes in Computer Science. Springer, 2010. http://dx.doi.org/10.1007/978-3-642-14335-9. [ bib | DOI ]
[76] Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors. Theoretical Aspects of Computing---ICTAC 2007, 4th International Colloquium, Macau, China, September 26--28, 2007, Proceedings, volume 4711 of Lecture Notes in Computer Science. Springer, 2007. [ bib ]
[77] Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors. Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24--25, 2007, volume 4700 of Lecture Notes in Computer Science. Springer, 2007. [ bib ]
[78] Chris George, Zhiming Liu, and Jim Woodcock, editors. Domain Modeling and the Duration Calculus, International Training School, Shanghai, China, September 17--21. 2007, Advanced Lectures, volume 4710 of Lecture Notes in Computer Science. Springer, 2007. [ bib ]
[79] Emine G. Aydal, Richard F. Paige, and Jim Woodcock. Evaluation of OCL for large-scale modelling: A different view of the Mondex purse. In Holger Giese, editor, Models in Software Engineering, Workshops and Symposia at MoDELS 2007, Nashville, TN, USA, September 30--October 5, 2007, Reports and Revised Selected Papers, volume 5002 of Lecture Notes in Computer Science, pages 194--205. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-69073-3_21. [ bib | DOI ]
[80] Andrew Butterfield, Adnan Sherif, and Jim Woodcock. Slotted-Circus. In Jim Davies and Jeremy Gibbons, editors, Integrated Formal Methods, 6th International Conference, IFM 2007, Oxford, UK, July 2--5, 2007, Proceedings, volume 4591 of Lecture Notes in Computer Science, pages 75--97. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-73210-5_5. [ bib | DOI ]
[81] Emine G. Aydal, Jim Woodcock, and Ana Cavalcanti. Goal-oriented automatic test case generators for MC/DC compliancy. In Joaquim Filipe, Boris Shishkov, and Markus Helfert, editors, ICSOFT 2007, Proceedings of the Second International Conference on Software and Data Technologies, Volume SE, Barcelona, Spain, July 22--25, 2007, pages 290--295. INSTICC Press, 2007. [ bib ]
[82] Juan Ignacio Perna and Jim Woodcock. A denotational semantics for Handel-C hardware compilation. In Michael J. Butler, Michael G. Hinchey, and María M. Larrondo-Petrie, editors, Formal Methods and Software Engineering, 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14--15, 2007, Proceedings, volume 4789 of Lecture Notes in Computer Science, pages 266--285. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-76650-6_16. [ bib | DOI ]
[83] Marcel Oliveira and Jim Woodcock. Automatic generation of verified concurrent hardware. In Michael J. Butler, Michael G. Hinchey, and María M. Larrondo-Petrie, editors, Formal Methods and Software Engineering, 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14--15, 2007, Proceedings, volume 4789 of Lecture Notes in Computer Science, pages 286--306. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-76650-6_17. [ bib | DOI ]
[84] Leo Freitas, Konstantinos Mokos, and Jim Woodcock. Verifying the CICS file control API with Z/Eves: An experiment in the verified software repository. In 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 10--14 July 2007, Auckland, New Zealand, pages 290--298. IEEE Computer Society, 2007. http://dx.doi.org/10.1109/ICECCS.2007.45. [ bib | DOI ]
[85] Leo Freitas, Zheng Fu, and Jim Woodcock. POSIX file store in Z/Eves: an experiment in the verified software repository. In 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 10--14 July 2007, Auckland, New Zealand, pages 3--14. IEEE Computer Society, 2007. http://dx.doi.org/10.1109/ICECCS.2007.36. [ bib | DOI ]
[86] Andrew Butterfield and Jim Woodcock. Formalising flash memory: First steps. In 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 10--14 July 2007, Auckland, New Zealand, pages 251--260. IEEE Computer Society, 2007. http://dx.doi.org/10.1109/ICECCS.2007.23. [ bib | DOI ]
[87] Leo Freitas and Jim Woodcock. Proving theorems about JML classes. In Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Papers presented at a Symposium held in Macao, China, September 24--25, 2007, volume 4700 of Lecture Notes in Computer Science, pages 255--279. Springer, 2007. http://dx.doi.org/10.1007/978-3-540-75221-9_11. [ bib | DOI ]
[88] Jim Woodcock and Richard Banach. The verification grand challenge. J. UCS, 13(5):661--668, 2007. http://dx.doi.org/10.3217/jucs-013-05-0661. [ bib | DOI ]
[89] Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. A denotational semantics for Circus. Electr. Notes Theor. Comput. Sci., 187:107--123, 2007. http://dx.doi.org/10.1016/j.entcs.2006.08.047. [ bib | DOI ]
[90] Leo Freitas and Jim Woodcock. FDR Explorer. Electr. Notes Theor. Comput. Sci., 187:19--34, 2007. http://dx.doi.org/10.1016/j.entcs.2006.08.042. [ bib | DOI ]
[91] Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone, editors. Theoretical Aspects of Computing---ICTAC 2006, Third International Colloquium, Tunis, Tunisia, November 20--24, 2006, Proceedings, volume 4281 of Lecture Notes in Computer Science. Springer, 2006. [ bib ]
[92] Jim Woodcock. An operational semantics in UTP for a language of reactive designs (abstract). In Steve Dunne and Bill Stoddart, editors, Unifying Theories of Programming, First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5--7, 2006, Revised Selected Papers, volume 4010 of Lecture Notes in Computer Science, pages 84--84. Springer, 2006. http://dx.doi.org/10.1007/11768173_5. [ bib | DOI ]
[93] Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. Unifying Theories in ProofPower-Z. In Steve Dunne and Bill Stoddart, editors, Unifying Theories of Programming, First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5--7, 2006, Revised Selected Papers, volume 4010 of Lecture Notes in Computer Science, pages 123--140. Springer, 2006. http://dx.doi.org/10.1007/11768173_8. [ bib | DOI ]
[94] Gift Nuka and Jim Woodcock. Mechanising a unifying theory. In Steve Dunne and Bill Stoddart, editors, Unifying Theories of Programming, First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5--7, 2006, Revised Selected Papers, volume 4010 of Lecture Notes in Computer Science, pages 217--235. Springer, 2006. http://dx.doi.org/10.1007/11768173_13. [ bib | DOI ]
[95] Ana Cavalcanti, Will Harwood, and Jim Woodcock. Pointers and records in the unifying theories of programming. In Steve Dunne and Bill Stoddart, editors, Unifying Theories of Programming, First International Symposium, UTP 2006, Walworth Castle, County Durham, UK, February 5--7, 2006, Revised Selected Papers, volume 4010 of Lecture Notes in Computer Science, pages 200--216. Springer, 2006. http://dx.doi.org/10.1007/11768173_12. [ bib | DOI | .pdf ]
We present a theory of pointers and records that provides a representation for objects and sharing in languages like Java and C++. Our approach to pointers is based on Paige's entity groups, which give an abstract view of storage as equivalence classes of variables that share the same memory location. We first define our theory as a restriction of the general theory of relations, and, as a consequence, it does not distinguish between terminating and non-terminating programs. Therefore, we link it with the theory of designs, providing a foundation for reasoning about total correctness of pointer-based sequential programs. Our work is a step towards the semantics of an object-oriented language that also integrates constructs for specifying state-rich and concurrent systems.

Keywords: semantics, refinement, relations, object models
[96] Jim Woodcock. First steps in the Verified Software Grand Challenge. In 30th Annual IEEE / NASA Software Engineering Workshop (SEW-30 2006), 25--28 April 2006, Loyola College Graduate Center, Columbia, MD, USA, pages 203--206. IEEE Computer Society, 2006. http://dx.doi.org/10.1109/SEW.2006.17. [ bib | DOI ]
[97] Jim Woodcock and Leo Freitas. Z/Eves and the Mondex electronic purse. In Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone, editors, Theoretical Aspects of Computing---ICTAC 2006, Third International Colloquium, Tunis, Tunisia, November 20--24, 2006, Proceedings, volume 4281 of Lecture Notes in Computer Science, pages 15--34. Springer, 2006. http://dx.doi.org/10.1007/11921240_2. [ bib | DOI ]
[98] Leo Freitas, Ana Cavalcanti, and Jim Woodcock. Taking our own medicine: Applying the refinement calculus to state-rich refinement model checking. In Zhiming Liu and Jifeng He, editors, Formal Methods and Software Engineering, 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1--3, 2006, Proceedings, volume 4260 of Lecture Notes in Computer Science, pages 697--716. Springer, 2006. http://dx.doi.org/10.1007/11901433_38. [ bib | DOI ]
[99] Steve Schneider, Helen Treharne, Ana Cavalcanti, and Jim Woodcock. A layered behavioural model of platelets. In 11th International Conference on Engineering of Complex Computer Systems (ICECCS 2006), 15--17 August 2006, Stanford, California, USA, pages 98--106. IEEE Computer Society, 2006. http://doi.ieeecomputersociety.org/10.1109/ICECCS.2006.80. [ bib | DOI | .pdf ]
There is great interest in the application of nanotechnology to medicine, but concerns for safety are paramount. We present a modelling technique based on CSP and B as a starting point for simulation of networks of nanorobots. The model and the simulations are central features of our proposed approach to the construction of safety cases for nanomedicine applications, and complex networks of cooperating components in general. Our work is based on a case study: the clotting behaviour of (artificial) platelets. We present a model, and discuss its analysis and uses.

[100] Jim Woodcock. Verified Software Grand Challenge. In Jayadev Misra, Tobias Nipkow, and Emil Sekerinski, editors, FM 2006: Formal Methods, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21--27, 2006, Proceedings, volume 4085 of Lecture Notes in Computer Science, pages 617--617. Springer, 2006. http://dx.doi.org/10.1007/11813040_45. [ bib | DOI ]
[101] Leo Freitas, Jim Woodcock, and Ana Cavalcanti. State-rich model checking. ISSE, 2(1):49--64, 2006. http://dx.doi.org/10.1007/s11334-006-0021-9. [ bib | DOI | .pdf ]
In this paper we survey the area of formal verification techniques, with emphasis on model checking due to its wide acceptance by both academia and industry. The major approaches and their characteristics are presented, together with the main problems faced while trying to apply them. With the increased complexity of systems, as well as interest in software correctness, the demand for more pow- erful automatic techniques is pushing the theories and tools towards integration. We discuss the state of the art in combining formal methods tools, mainly model checking with theorem proving and abstract interpretation. In particular, we present our own recent contribution on an approach to integrate model checking and theorem proving to handle staterich systems specified using a combination of Z and CSP.

Keywords: model checking, theorem proving, abstract interpretation, formal method tools
[102] Ana Cavalcanti, Jim Woodcock, and Steve Dunne. Angelic nondeterminism in the unifying theories of programming. Formal Asp. Comput., 18(3):288--307, 2006. http://dx.doi.org/10.1007/s00165-006-0001-8. [ bib | DOI | .pdf ]
Hoare and He's unifying theories of programming (UTP) is a model of alphabetised relations expressed as predicates; it supports development in several programming paradigms. The aim of Hoare and He's work is the unification of languages and techniques, so that we can benefit from results in different contexts. In this paper, we investigate the integration of angelic nondeterminism in the UTP; we propose the unification of a model of binary multirelations, which is isomorphic to the monotonic predicate transformers model and can express angelic and demonic nondeterminism.

Keywords: semantics, refinement, relations, predicate transformers
[103] Juan Bicarregui, C. A. R. Hoare, and J. C. P. Woodcock. The verified software repository: a step towards the verifying compiler. Formal Asp. Comput., 18(2):143--151, 2006. http://dx.doi.org/10.1007/s00165-005-0079-4. [ bib | DOI ]
[104] Andrew Butterfield and Jim Woodcock. A "hardware compiler" semantics for Handel-C. Electr. Notes Theor. Comput. Sci., 161:73--90, 2006. http://dx.doi.org/10.1016/j.entcs.2006.04.026. [ bib | DOI ]
[105] Jim Woodcock. First steps in the Verified Software Grand Challenge. IEEE Computer, 39(10):57--64, 2006. http://dx.doi.org/10.1109/MC.2006.340. [ bib | DOI ]
[106] Cliff B. Jones, Peter W. O'Hearn, and Jim Woodcock. Verified software: A grand challenge. IEEE Computer, 39(4):93--95, 2006. http://dx.doi.org/10.1109/MC.2006.145. [ bib | DOI ]
[107] Bertrand Meyer and Jim Woodcock, editors. Verified Software: Theories, Tools, Experiments, First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10--13, 2005, Revised Selected Papers and Discussions, volume 4171 of Lecture Notes in Computer Science. Springer, 2008. http://dx.doi.org/10.1007/978-3-540-69149-5. [ bib | DOI ]
[108] Jim Woodcock, Ana Cavalcanti, and Leonardo Freitas. Operational semantics for model checking Circus. In John S. Fitzgerald, Ian J. Hayes, and Andrzej Tarlecki, editors, FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18--22, 2005, Proceedings, volume 3582 of Lecture Notes in Computer Science, pages 237--252. Springer, 2005. http://dx.doi.org/10.1007/11526841_17. [ bib | DOI | .pdf ]
Circus is a combination of Z, CSP, and the refinement calculus, and is based on Hoare & He's Unifying Theories of Programming. A model checker is being constructed for the language to conduct refinement checking in the style of FDR, but supported by theorem proving for reasoning about the complex states and data types that arise from the use of Z. FDR deals with bounded labelled transition systems (LTSs), but the Circus model checker manipulates LTSs with possibly infinite inscriptions on arcs and in nodes, and so, in general, the success or failure of a refinement check depends on interaction with a theorem prover. An LTS is generated from a source text using an operational interpretation of Circus; we present a Structured Operational Semantics for Circus, including both its process-algebraic and state-rich features.

[109] Andrew Butterfield and Jim Woodcock. prialt in Handel-C: an operational semantics. STTT, 7(3):248--267, 2005. http://dx.doi.org/10.1007/s10009-004-0181-6. [ bib | DOI ]
[110] Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock. Unifying classes and processes. Software and System Modeling, 4(3):277--296, 2005. http://dx.doi.org/10.1007/s10270-005-0085-2. [ bib | DOI | .pdf ]
Previously, we presented Circus, an integration of Z, CSP, and Morgan's refinement calculus, with a semantics based on the unifying theories of programming. Circus provides a basis for development of state-rich concurrent systems; it has a formal semantics, a refinement theory, and a development strategy. The design of Circus is our solution to combining data and behavioural specifications. Here, we further explore this issue in the context of object-oriented features. Concretely, we present an object-oriented extension of Circus called OhCircus. We present its syntax, describe its semantics, explain the formalisation of method calls, and discuss our approach to refinement.

[111] Ana Cavalcanti and Jim Woodcock. Angelic nondeterminism and unifying theories of programming. Electr. Notes Theor. Comput. Sci., 137(2):45--66, 2005. http://dx.doi.org/10.1016/j.entcs.2005.04.024. [ bib | DOI ]
[112] Diyaa-Addein Atiya, Steve King, and Jim Woodcock. Simpler reasoning about system properties: a proof-by-refinement technique. Electr. Notes Theor. Comput. Sci., 137(2):5--22, 2005. http://dx.doi.org/10.1016/j.entcs.2005.04.022. [ bib | DOI ]
[113] Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock, editors. Refinement Techniques in Software Engineering, First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised Lectures, volume 3167 of Lecture Notes in Computer Science. Springer, 2006. [ bib ]
[114] Xinbei Tang and Jim Woodcock. Towards mobile processes in unifying theories. In 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 28--30 September 2004, Beijing, China, pages 44--53. IEEE Computer Society, 2004. http://doi.ieeecomputersociety.org/10.1109/SEFM.2004.49. [ bib | DOI ]
[115] Ana Cavalcanti and Jim Woodcock. A tutorial introduction to CSP in Unifying Theories of Programming. In Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock, editors, Refinement Techniques in Software Engineering, First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised Lectures, volume 3167 of Lecture Notes in Computer Science, pages 220--268. Springer, 2004. http://dx.doi.org/10.1007/11889229_6. [ bib | DOI | .pdf ]
In their Unifying Theories of Programming, Hoare & He use the alphabetised relational calculus to give denotational semantics to a wide variety of constructs taken from different programming paradigms. We give a tutorial introduction to the semantics of CSP processes. We start with a summarised introduction of the alphabetised relational calculus and the theory of designs, which are precondition-postcondition specifications. Afterwards, we present in detail a theory for reactive processes. Later, we combine the theories of designs and reactive processes to provide the model for CSP processes. Finally, we compare this new model with the standard failures-divergences model for CSP.

[116] Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock. Refinement: An overview. In Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock, editors, Refinement Techniques in Software Engineering, First Pernambuco Summer School on Software Engineering, PSSE 2004, Recife, Brazil, November 23-December 5, 2004, Revised Lectures, volume 3167 of Lecture Notes in Computer Science, pages 1--17. Springer, 2004. http://dx.doi.org/10.1007/11889229_1. [ bib | DOI ]
[117] Xinbei Tang and Jim Woodcock. Travelling Processes. In Dexter Kozen and Carron Shankland, editors, Mathematics of Program Construction, 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12--14, 2004, Proceedings, volume 3125 of Lecture Notes in Computer Science, pages 381--399. Springer, 2004. http://dx.doi.org/10.1007/978-3-540-27764-4_20. [ bib | DOI ]
[118] Jim Woodcock and Ana Cavalcanti. A tutorial introduction to designs in unifying theories of programming. In Eerke A. Boiten, John Derrick, and Graeme Smith, editors, Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 4--7, 2004, Proceedings, volume 2999 of Lecture Notes in Computer Science, pages 40--66. Springer, 2004. http://dx.doi.org/10.1007/978-3-540-24756-2_4. [ bib | DOI | .pdf ]
In their Unifying Theories of Programming (UTP), Hoare & He use the alphabetised relational calculus to give denotational semantics to a wide variety of constructs taken from different programming paradigms. A key concept in their programme is the design: the familiar precondition-postcondition pair that describes the contract between a programmer and a client. We give a tutorial introduction to the theory of alphabetised relations, and its sub-theory of designs. We illustrate the ideas by applying them to theories of imperative programming, including Hoare logic, weakest preconditions, and the refinement calculus.

[119] Alistair A. McEwan and J. C. P. Woodcock. A refinement based approach to calculating a fault tolerant railway signal device. In René Jacquart, editor, Building the Information Society, IFIP 18th World Computer Congress, Topical Sessions, 22--27 August 2004, Toulouse, France, volume 156 of IFIP, pages 621--627. Kluwer/Springer, 2004. http://dx.doi.org/10.1007/978-1-4020-8157-6_60. [ bib | DOI ]
[120] Jim Woodcock. Using Circus for safety-critical applications. Electr. Notes Theor. Comput. Sci., 95:3--22, 2004. http://dx.doi.org/10.1016/j.entcs.2004.04.003. [ bib | DOI ]
[121] Gift Nuka and Jim Woodcock. Mechanising the alphabetised relational calculus. Electr. Notes Theor. Comput. Sci., 95:209--225, 2004. http://dx.doi.org/10.1016/j.entcs.2004.04.013. [ bib | DOI ]
[122] Jin Song Dong and Jim Woodcock, editors. Formal Methods and Software Engineering, 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5--7, 2003, Proceedings, volume 2885 of Lecture Notes in Computer Science. Springer, 2003. [ bib ]
[123] Diyaa-Addein Atiya, Steve King, and Jim Woodcock. A Circus semantics for Ravenscar protected objects. In Keijiro Araki, Stefania Gnesi, and Dino Mandrioli, editors, FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8--14, 2003, Proceedings, volume 2805 of Lecture Notes in Computer Science, pages 617--635. Springer, 2003. http://dx.doi.org/10.1007/978-3-540-45236-2_34. [ bib | DOI ]
[124] Ana Cavalcanti and Jim Woodcock. Predicate transformers in the semantics of Circus. IEE Proceedings---Software, 150(2):85--94, 2003. http://dx.doi.org/10.1049/ip-sen:20030131. [ bib | DOI | .pdf ]
Circus is a combination of Z and CSP; its chief distinguishing feature is the inclusion of the ideas of the refinement calculus. Our main objective is the definition of refinement methods for concurrent programs. The original semantic model for Circus is Hoare and He's unifying theories of programming. In this paper, we present an equivalent semantics based on predicate transformers. With this new model, we provide a more adequate basis for the formalisation of refinement and verification-condition generation rules. Furthermore, this new framework makes it possible to include logical variables and angelic nondeterminism in Circus. The consistency of the relational and predicate transformer models gives us confidence in their accuracy.

[125] Marcel Oliveira, Ana Cavalcanti, and Jim Woodcock. Arcangel: a tactic language for refinement. Formal Asp. Comput., 15(1):28--47, 2003. http://dx.doi.org/10.1007/s00165-003-0003-8. [ bib | DOI ]
[126] Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock. A refinement strategy for Circus. Formal Asp. Comput., 15(2--3):146--181, 2003. http://dx.doi.org/10.1007/s00165-003-0006-5. [ bib | DOI | .pdf ]
We present a refinement strategy for Circus, which is the combination of Z, CSP, and the refinement calculus in the setting of Hoare & He's unifying theories of programming. The strategy unifies the theories of refinement for processes and their constituent actions, and provides a coherent technique for the stepwise refinement of concurrent and distributed programs involving rich data structures. This kind of development is carried out using Circus's refinement calculus, and we describe some of its laws for the simultaneous refinement of state and control behaviour, including the splitting of a process into parallel subcomponents. We illustrate the strategy and the laws using a case study that shows the complete development of a small distributed program.

[127] Andrew Butterfield and Jim Woodcock. An operational semantics for Handel-C. Electr. Notes Theor. Comput. Sci., 80:235--250, 2003. http://dx.doi.org/10.1016/S1571-0661(04)80821-1. [ bib | DOI ]
[128] Jim Woodcock and Ana Cavalcanti. The semantics of Circus. In Didier Bert, Jonathan P. Bowen, Martin C. Henson, and Ken Robinson, editors, ZB 2002: Formal Specification and Development in Z and B, 2nd International Conference of B and Z Users, Grenoble, France, January 23--25, 2002, Proceedings, volume 2272 of Lecture Notes in Computer Science, pages 184--203. Springer, 2002. http://dx.doi.org/10.1007/3-540-45648-1_10. [ bib | DOI | .pdf ]
Circus is a concurrent language for refinement; it is a unification of imperative CSP, Z, and the refinement calculus. We describe the language of Circus and the formulation of its model in Hoare & He's unifying theories of programming.

[129] Jim Woodcock and Arthur P. Hughes. Unifying theories of parallel programming. In Chris George and Huaikou Miao, editors, Formal Methods and Software Engineering, 4th International Conference on Formal Engineering Methods, ICFEM 2002 Shanghai, China, October 21--25, 2002, Proceedings, volume 2495 of Lecture Notes in Computer Science, pages 24--37. Springer, 2002. http://dx.doi.org/10.1007/3-540-36103-0_5. [ bib | DOI ]
[130] Augusto Sampaio, Jim Woodcock, and Ana Cavalcanti. Refinement in Circus. In Lars-Henrik Eriksson and Peter A. Lindsay, editors, FME 2002: Formal Methods---Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22--24, 2002, Proceedings, volume 2391 of Lecture Notes in Computer Science, pages 451--470. Springer, 2002. http://dx.doi.org/10.1007/3-540-45614-7_26. [ bib | DOI | .pdf ]
We describe refinement in Circus, a concurrent specification language that integrates imperative CSP, Z, and the refinement calculus. Each Circus process has a state and accompanying actions that define both the internal state transitions and the changes in control flow that occur during execution. We define the meaning of refinement of processes and their actions, and propose a sound data refinement technique for process refinement. Refinement laws for CSP and Z are directly relevant and applicable to Circus, but our focus here is on new laws for processes that integrate state and control. We give some new results about the distribution of data refinement through the combinators of CSP. We illustrate our ideas with the development of a distributed system of cooperating processes from a centralised specification.

Keywords: Z, CSP, distribution, unifying theories of programming
[131] John Derrick, Eerke A. Boiten, Jim Woodcock, and Joakim von Wright. Preface. Electr. Notes Theor. Comput. Sci., 70(3):1--2, 2002. http://dx.doi.org/10.1016/S1571-0661(05)80478-5. [ bib | DOI ]
[132] Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock. Refinement of actions in Circus. Electr. Notes Theor. Comput. Sci., 70(3):132--162, 2002. http://dx.doi.org/10.1016/S1571-0661(05)80489-X. [ bib | DOI ]
[133] Andrew Butterfield and Jim Woodcock. Semantic domains for Handel-C. Electr. Notes Theor. Comput. Sci., 74:1--20, 2002. http://dx.doi.org/10.1016/S1571-0661(04)80762-X. [ bib | DOI ]
[134] Jim Woodcock and Ana Cavalcanti. A concurrent language for refinement. In Andrew Butterfield, Glenn Strong, and Claus Pahl, editors, 5th Irish Workshop on Formal Methods, IWFM 2001, Dublin, Ireland, 16--17 July 2001, Workshops in Computing. BCS, 2001. http://ewic.bcs.org/content/ConWebDoc/4146. [ bib ]
[135] Jim Woodcock and Ana Cavalcanti. The steam boiler in a unified theory of Z and CSP. In 8th Asia-Pacific Software Engineering Conference (APSEC 2001), 4--7 December 2001, Macau, China, pages 291--298. IEEE Computer Society, 2001. http://dx.doi.org/10.1109/APSEC.2001.991490. [ bib | DOI ]
[136] Jeannette M. Wing and Jim Woodcock. Guest editors' introduction-special issues for FM '99: The first world congress on formal methods in the development of computing systems. IEEE Trans. Software Eng., 26(8):673--674, 2000. http://dx.doi.org/10.1109/TSE.2000.879806. [ bib | DOI ]
[137] Jeannette M. Wing and Jim Woodcock. Introduction: Special issues for fm'99, the first world congress on formal methods in the development of computing systems. Formal Methods in System Design, 17(3):199--200, 2000. http://dx.doi.org/10.1023/A:1026521916117. [ bib | DOI ]
[138] Jeannette M. Wing and Jim Woodcock. The first world congress on formal methods in the development of computing systems. Formal Asp. Comput., 12(3):145--146, 2000. http://dx.doi.org/10.1007/PL00011167. [ bib | DOI ]
[139] Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors. FM'99---Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20--24, 1999, Proceedings, Volume II, volume 1709 of Lecture Notes in Computer Science. Springer, 1999. [ bib ]
[140] Jeannette M. Wing, Jim Woodcock, and Jim Davies, editors. FM'99---Formal Methods, World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20--24, 1999, Proceedings, Volume I, volume 1708 of Lecture Notes in Computer Science. Springer, 1999. [ bib ]
[141] Charles Crichton, Jim Davies, and Jim Woodcock. When to trust mobile objects: Access control in the jini(tm) software system. In Donald Firesmith, Richard Riehle, Gilda Pour, and Bertrand Meyer, editors, TOOLS 1999: 30th International Conference on Technology of Object-Oriented Languages and Systems, Delivering Quality Software---The Way Ahead, 1--5 August 1999, Santa Barbara, CA, USA, pages 116--125. IEEE Computer Society, 1999. http://dx.doi.org/10.1109/TOOLS.1999.787541. [ bib | DOI ]
[142] Christie Bolton, Jim Davies, and Jim Woodcock. On the refinement and simulation of data types and processes. In Keijiro Araki, Andy Galloway, and Kenji Taguchi, editors, Integrated Formal Methods, Proceedings of the 1st International Conference on Integrated Formal Methods, IFM 99, York, UK, 28--29 June 1999, pages 273--292. Springer, 1999. [ bib ]
[143] Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock. An inconsistency in procedures, parameters, and substitution in the refinement calculus. Sci. Comput. Program., 33(1):87--96, 1999. http://dx.doi.org/10.1016/S0167-6423(97)00015-4. [ bib | DOI ]
[144] Susan Stepney, David Cooper, and Jim Woodcock. More powerful Z data refinement: Pushing the state of the art in industrial refinement. In Jonathan P. Bowen, Andreas Fett, and Michael G. Hinchey, editors, ZUM '98: The Z Formal Specification Notation, 11th International Conference of Z Users, Berlin, Germany, September 24--26, 1998, Proceedings, volume 1493 of Lecture Notes in Computer Science, pages 284--307. Springer, 1998. http://dx.doi.org/10.1007/978-3-540-49676-2_20. [ bib | DOI ]
[145] Ana Cavalcanti, Augusto Sampaio, and Jim Woodcock. Procedures and recursion in the refinement calculus. J. Braz. Comp. Soc., 5(1), 1998. [ bib ]
[146] Ana Cavalcanti and Jim Woodcock. ZRC---A refinement calculus for Z. Formal Asp. Comput., 10(3):267--289, 1998. http://dx.doi.org/10.1007/s001650050016. [ bib | DOI ]
[147] Ana Cavalcanti and Jim Woodcock. A weakest precondition semantics for Z. Comput. J., 41(1):1--15, 1998. http://dx.doi.org/10.1093/comjnl/41.1.1. [ bib | DOI ]
[148] Marie-Claude Gaudel and Jim Woodcock, editors. FME '96: Industrial Benefit and Advances in Formal Methods, Third International Symposium of Formal Methods Europe, Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18--22, 1996, Proceedings, volume 1051 of Lecture Notes in Computer Science. Springer, 1996. [ bib ]
[149] A. W. Roscoe, Jim Woodcock, and L. Wulf. Non-interference through determinism. Journal of Computer Security, 4(1):27--54, 1996. http://dx.doi.org/10.3233/JCS-1996-4103. [ bib | DOI ]
[150] A. P. Martin, Paul H. B. Gardiner, and Jim Woodcock. A tactic calculus---abridged version. Formal Asp. Comput., 8(4):479--489, 1996. http://dx.doi.org/10.1007/BF01213535. [ bib | DOI ]
[151] Jim Woodcock. Software engineering research directions. ACM Comput. Surv., 28(4es):128, 1996. http://doi.acm.org/10.1145/242224.242387. [ bib | DOI ]
[152] Jane Sinclair and Jim Woodcock. Event refinement in state-based concurrent systems. Formal Asp. Comput., 7(3):266--288, 1995. http://dx.doi.org/10.1007/BF01211074. [ bib | DOI ]
[153] Jonathan P. Bowen and J. A. Hall, editors. Z User Workshop, Cambridge, UK, 29--30 June 1994, Proceedings, Workshops in Computing. Springer/BCS, 1994. [ bib ]
[154] Jim Woodcock, Paul H. B. Gardiner, and J. R. Hulance. The formal specification in Z of Defence Standard 00--56. In Jonathan P. Bowen and J. A. Hall, editors, Z User Workshop, Cambridge, UK, 29--30 June 1994, Proceedings, Workshops in Computing, pages 9--28. Springer/BCS, 1994. [ bib ]
[155] A. W. Roscoe, Jim Woodcock, and L. Wulf. Non-interference through determinism. In Dieter Gollmann, editor, Computer Security---ESORICS 94, Third European Symposium on Research in Computer Security, Brighton, UK, November 7--9, 1994, Proceedings, volume 875 of Lecture Notes in Computer Science, pages 33--53. Springer, 1994. http://dx.doi.org/10.1007/3-540-58618-0_55. [ bib | DOI ]
[156] Jim Woodcock and Peter Gorm Larsen, editors. FME '93: Industrial-Strength Formal Methods, First International Symposium of Formal Methods Europe, Odense, Denmark, April 19--23, 1993, Proceedings, volume 670 of Lecture Notes in Computer Science. Springer, 1993. [ bib ]
[157] Richard S. Bird, Carroll Morgan, and Jim Woodcock, editors. Mathematics of Program Construction, Second International Conference, Oxford, U.K., June 29--July 3, 1992, Proceedings, volume 669 of Lecture Notes in Computer Science. Springer, 1993. [ bib ]
[158] Jim Woodcock. The rudiments of algorithm refinement. Comput. J., 35(5):441--450, 1992. http://dx.doi.org/10.1093/comjnl/35.5.441. [ bib | DOI ]
[159] Jim Woodcock. Two refinement case studies. In Søren Prehn and W. J. Toetenel, editors, VDM '91---Formal Software Development, 4th International Symposium of VDM Europe, Noordwijkerhout, The Netherlands, October 21--25, 1991, Proceedings, Volume 2: Tutorials, volume 552 of Lecture Notes in Computer Science, pages 118--140. Springer, 1991. [ bib ]
[160] Jim Woodcock. An introduction to refinement in Z. In Søren Prehn and W. J. Toetenel, editors, VDM '91---Formal Software Development, 4th International Symposium of VDM Europe, Noordwijkerhout, The Netherlands, October 21--25, 1991, Proceedings, Volume 2: Tutorials, volume 552 of Lecture Notes in Computer Science, pages 96--117. Springer, 1991. [ bib ]
[161] Jim Woodcock. The refinement calculus. In Søren Prehn and W. J. Toetenel, editors, VDM '91---Formal Software Development, 4th International Symposium of VDM Europe, Noordwijkerhout, The Netherlands, October 21--25, 1991, Proceedings, Volume 2: Tutorials, volume 552 of Lecture Notes in Computer Science, pages 80--95. Springer, 1991. [ bib ]
[162] Jim Woodcock. A tutorial on the refinement calculus. In Søren Prehn and W. J. Toetenel, editors, VDM '91---Formal Software Development, 4th International Symposium of VDM Europe, Noordwijkerhout, The Netherlands, October 21--25, 1991, Proceedings, Volume 2: Tutorials, volume 552 of Lecture Notes in Computer Science, pages 79--140. Springer, 1991. http://dx.doi.org/10.1007/BFb0019996. [ bib | DOI ]
[163] Paul H. B. Gardiner, P. J. Lupton, and Jim Woodcock. A simpler semantics for Z. In J. E. Nicholls, editor, Z User Workshop, Oxford, UK, Proceedings of the Fifth Annual Z User Meeting, 17--18 December 1990, Workshops in Computing, pages 3--11. Springer, 1990. [ bib ]
[164] Jim Woodcock and Carroll Morgan. Refinement of state-based concurrent systems. In Dines Bjørner, C. A. R. Hoare, and Hans Langmaack, editors, VDM '90, VDM and Z---Formal Methods in Software Development, Third International Symposium of VDM Europe, Kiel, FRG, April 17--21, 1990, Proceedings, volume 428 of Lecture Notes in Computer Science, pages 340--351. Springer, 1990. http://dx.doi.org/10.1007/3-540-52513-0_18. [ bib | DOI ]
[165] J. C. P. Woodcock. Structuring specifications in Z. Software Engineering Journal, 4(1):51--66, 1989. http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=28090. [ bib ]
[166] Jim Woodcock and B. Dickinson. Using VDM with rely and guarantee-conditions---experiences from a real project. In Robin E. Bloomfield, Lynn S. Marshall, and Roger B. Jones, editors, VDM '88, VDM---The Way Ahead, 2nd VDM-Europe Symposium, Dublin, Ireland, September 11--16, 1988, Proceedings, volume 328 of Lecture Notes in Computer Science, pages 434--458. Springer, 1988. http://dx.doi.org/10.1007/3-540-50214-9_27. [ bib | DOI ]
[167] Bernard Sufrin and Jim Woodcock. Towards the formal specification of a simple programming support environment. Software Engineering Journal, 2(4):86--94, 1987. http://dx.doi.org/10.1049/sej.1987.0012. [ bib | DOI ]

This file was generated by bibtex2html 1.98.