Abstract Autonomous agents are increasingly deployed in sensitive, human-centric domains—such as healthcare, assistive care, and emergency response—where their decision-making must align with complex human norms. These translate into Social, Legal, Ethical, Empathetic, and Cultural (SLEEC) requirements that are often nuanced and context-dependent, challenging traditional software engineering paradigms. Our tutorial paper presents a comprehensive, tool-supported methodology for managing the SLEEC requirements lifecycle, covering elicitation, well-formedness validation, and conformance verification of software design models against SLEEC requirements. We demonstrate the use of our methodology and associated tools through application to a robot-assisted dressing system, providing a guide for researchers and engineers to bridge the gap between abstract human norms and verifiable system designs.

We present a theorem-proving-based technique for verifying deadlock freedom of CSP-style concurrent models in Isabelle/HOL. The approach addresses challenges that are difficult to handle using model checking alone, including infinite state spaces, compositional reasoning in the presence of shared variables, and the need for mechanised proofs. Our main contribution is a coinductive characterisation of deadlock freedom that is equivalent to the standard CSP refinement-based definition, but is more amenable to automated reasoning in an interactive theorem prover. To support reasoning about shared variables, we introduce an assume–guarantee strategy that enforces invariants within transition semantics. The technique is generally applicable to CSP specifications that model shared variables using standard CSP constructs. In particular, we consider the semantics of RoboChart, a domain-specific modelling language for robotic control software, which we mechanise in Isabelle via a shallow embedding in HOL-CSP, and implement automated proof methods. The approach is evaluated on three case studies, including two RoboChart models of industrial robotic systems.

There is extensive literature on automated test generation using reactive design models, where control is determined by events. In contrast, the (idealised) simulation paradigm defines control through cycles dictated by the passage of time. Within each cycle, inputs are read and processed, and outputs are provided, all instantaneously, and afterwards time progresses. To exercise a simulation using tests generated from a reactive design model requires changes to the tests to take into account this paradigm shift. This article focuses on automation of the necessary changes and of the use of the resulting tests in a simulation campaign. Based on a notion of conformance that establishes whether a simulation is correct with respect to a reactive design, we (1) identify the reactive tests that are meaningful; (2) define a process to convert those tests; (3) provide an algorithm to execute those tests and (4) prove soundness and completeness of our approach. Our work is described in the context of the RoboStar framework for model-based development of control software for robotics applications, and its process algebraic semantics. The testing approach we propose here represents a significant advancement in the current testing practices within the field of robotics, where simulations are widely used.

Abstract It is often the case that a robot must adapt to unexpected changes in its environment. It is, however, important that these changes can be demonstrated to maintain the safe operation of the robot. The adaptive systems community has developed the MAPE-K pattern as a widely recognised conceptual architecture. We propose extending MAPE-K to incorporate runtime verification, resulting in an architecture we call MAPLE-K. In this paper, we capture and formalise both the MAPE-K and MAPLE-K architectures using a domain-specific language. Additionally, we provide support for translation from architectural models to software models and code to facilitate the deployment of verified applications. MAPE-K is rarely maintained at the implementation level, but our work ensures traceability between the code and its design, enabling the use of architectural information to verify the correctness of the software.

Abstract Proving properties about robotic systems with humans-in-the-loop relies on assumptions about human behaviour. Existing technologies require expertise not reasonably expected from psychologists and human-factors engineers, for instance. A user-needs analysis of industrial design techniques for human-robot interaction has identified a lack of standardised approach. We present RoboScene, a notation based on UML sequence diagrams that can be used to capture assumptions derived from human-factors artefacts, through novel constructs enabling consideration of stakeholders with different traits. We describe a tock-CSP semantics for RoboScene, and show how we can connect (mathematically) RoboScene diagrams to platform-independent software models. This is applied in the context of a Human-Centered Engineering process, demonstrated via an industrial case study.

Autonomous agents are increasingly being proposed for use in healthcare, assistive care, education, and other applications governed by complex human-centric norms. To ensure compliance with these norms, the rules they induce need to be unambiguously defined, checked for consistency, and used to verify the agent. In this paper, we introduce a framework for formal specification, validation and verification of social, legal, ethical, empathetic and cultural (SLEEC) rules for autonomous agents. Our framework comprises: (i) a language for specifying SLEEC rules and rule defeaters (that is, circumstances in which a rule does not apply or an alternative form of the rule is required); (ii) a formal semantics (defined in the process algebra tock-CSP) for the language; and (iii) methods for detecting conflicts and redundancy within a set of rules, and for verifying the compliance of an autonomous agent with such rules. We show the applicability of our framework for two autonomous agents from different domains: a firefighter UAV, and an assistive-dressing robot.

Simulation is a favoured technique in robotics. It is, however, costly, in terms of development time, and its usability is limited by the lack of standardisation and portability of simulators. We present RoboSim, a diagrammatic tool-independent domain-specific language to model robotic platforms and their controllers. It can be regarded as a profile of UML/SysML enriched with time primitives, differential equations, and a mathematical semantics. Our previous work on RoboSim described a notation to specify control software. In this paper, we present a novel notation to describe physical models: block diagrams that can be linked to the platform-independent software model to characterise how services required by the software are realised by actuators and sensors. Behaviours are specified by differential equations, and simulations and mathematical models of the whole system can be generated automatically. Our main contributions are a modular and extensible diagrammatic notation that supports the explicit specification of physical behaviours; a set of validation rules that identify well-formed models; a model-to-model transformation from RoboSim to an input format accepted by several simulators; and a formal semantics for mathematical reasoning.

As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this difficult task, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues, such as conflicts, redundancy, restrictiveness, and insufficiency, yielding diagnostics that pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs, comprising 62 issues for the software underpinning the operation of systems, such as, assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.

Normative non-functional requirements specify con-straints that a system must observe in order to avoid violations of social, legal, ethical, empathetic, and cultural norms. As these requirements are typically defined by non-technical system stakeholders with different expertise and priorities (ethicists, lawyers, social scientists, etc.), ensuring their well-formedness and consistency is very challenging. Recent research has tackled this challenge using a domain-specific language to specify normative requirements as rules whose consistency can then be analysed with formal methods. In this paper, we propose a complemen-tary approach that uses Large Language Models to extract semantic relationships between abstract representations of system capabilities. These relations, which are often assumed implicitly by non-technical stakeholders (e.g., based on common sense or domain knowledge), are then used to enrich the automated reasoning techniques for eliciting and analyzing the consistency of normative requirements. We show the effectiveness of our approach to normative requirements elicitation and operational-ization through a range of real-world case studies. An extended version of this paper, which includes appendices is available at https://arxiv.org/abs/2404.12335

Abstract State machines are widely used in industry and academia to capture behavioural models of control. They are included in popular notations, such as UML and its variants, and used (sometimes informally) to describe computational artefacts. In this paper, we present laws for state machines that we prove sound with respect to a process algebraic semantics for refinement, and complete, in that they are sufficient to reduce an arbitrary model to a normal form that isolates basic (action and control) elements. We consider two variants of UML-like state machines, both enriched with facilities to deal with time budgets, timeouts and deadlines over triggers and actions. In the first variant, machines are self-contained components, declaring all the variables, events and operations that they require or define. In contrast, in the second variant, machines are open, like in UML for instance. Laws for open state machines do not depend on a specific context of variables, events and operations, and normalization uses a novel operator for open-machine (de)composition. Our laws can be used in behaviour-preservation transformation techniques. Their applications are automated by a model-transformation engine.

A growing range of applications use AI and other autonomous agents to perform tasks that raise social, legal, ethical, empathetic, and cultural (SLEEC) concerns. To support a framework for the consideration of these concerns, we introduce SLEEC-TK, a toolkit for specification, validation, and verification of SLEEC requirements. SLEEC-TK is an Eclipse-based environment for defining SLEEC rules in a domain-specific language with a timed process algebraic semantics. SLEEC-TK uses model checking to identify redundant and conflicting rules, and to verify conformance of design models with SLEEC rules. We illustrate the use of SLEEC-TK for an assistive-care robot.

Advances in Artificial Intelligence (AI), and in particular in Machine Learning (ML), are introducing profound changes to scholarly submissions across publication venues, affecting in particular the contributions that are being submitted to Software Engineering (SE) conferences and journals. In this context, it is not always clear whether manuscripts submitted to SE venues under the umbrella term SE for AI are indeed relevant to SE, in the sense that they explicitly contain contributions to the SE body of knowledge. This leads to recurring discussions on whether certain AI-related submissions are appropriate to SE venues, or should instead be submitted to other journals and conferences, including AI or ML-specific ones. In this editorial, we discuss the kinds of AI-related contributions that are a better fit-and a less good fit-for publication in the IEEE Transactions on Software Engineering.

Abstract A growing range of applications use autonomous agents such as AI and robotic systems to perform tasks deemed dangerous, tedious or costly for humans. To truly succeed with these tasks, the autonomous agents must perform them without violating the social, legal, ethical, empathetic, and cultural (SLEEC) norms of their users and operators. We introduce SLEECVAL, a tool for specification and validation of rules that reflect these SLEEC norms. Our tool supports the specification of SLEEC rules in a DSL [1] we co-defined with the help of ethicists, lawyers and stakeholders from health and social care, and uses the CSP refinement checker FDR4 to identify redundant and conflicting rules in a SLEEC specification. We illustrate the use of SLEECVAL for two case studies: an assistive dressing robot, and a firefighting drone.

The state of practice in design and verification of control software for robotics is code centric. The RoboStar framework supports a model-based approach, providing support for modelling and simulation, and techniques for automatic generation of artefacts. Existing results support test generation using a reactive design model; in RoboStar such models can be described using a diagrammatic notation called RoboChart. Here, we describe the challenges involved in using such tests for execution against simulations or cyclic implementations either automatically generated or custom developed. While it is possible to use a cyclic model to generate tests in the first place, reactive models are akin to those normally used by the community. Moreover, by linking design-based tests to the tests executed against the cyclic mechanisms, we support traceability.

As software and cyber-physical systems interacting with humans become prevalent in domains such as healthcare, education and customer service, software engineers need to consider normative (i.e., social, legal, ethical, empathetic and cultural) requirements. However, their elicitation is challenging, as they must reflect the often conflicting or redundant views of stakeholders ranging from users and operators to lawyers, ethicists and regulators. To address this challenge, we introduce a tool-supported Formal framework for normaTive requirements elicitation (FormaTive). It allows specification of normative rules for a software system in an intuitive high-level language, and automates: (i) the mapping of the rules to an internal formal representation; (ii) their analysis to identify rule conflicts, redundancies, and concerns; and (iii) the synthesis of feedback enabling users to understand and resolve problems.

A robot affects and is affected by its environment, so that typically its behaviour depends on properties of that environment. For verification, we need to formalise those properties. Modelling the environment is very challenging, if not impossible, but we can capture assumptions. Here, we present RoboWorld, a domain-specific controlled natural language with a process algebraic semantics that can be used to define (a) operational requirements, and (b) environment interactions of a robot. RoboWorld is part of the RoboStar framework for verification of robotic systems. In this article, we define RoboWorld’s syntax and hybrid semantics, and illustrate its use for capturing operational requirements, for automatic test generation, and for proof. We also present a tool that supports the writing of RoboWorld documents. Since RoboWorld is a controlled natural language, it complements the other RoboStar notations in being accessible to roboticists, while at the same time benefitting from a formal semantics to support rigorous verification (via testing and proof).

The existing testing theories for CSP cater for verification of interaction patterns (traces) and deadlocks, but not time. We address here refinement and testing based on a dialect of CSP, called tock -CSP, which can capture discrete time properties. This version of CSP has been of widespread interest for decades; recently, it has been given a denotational semantics, and model checking has become possible using a well established tool. Here, we first equip tock -CSP with a novel semantics for testing, which distinguishes input and output events: the standard models of ( tock -)CSP do not differentiate them, but for testing this is essential. We then present a new testing theory for timewise refinement, based on novel definitions of test and test execution. Finally, we reconcile refinement and testing by relating timed ioco testing and refinement in tock -CSP with inputs and outputs. With these results, this paper provides, for the first time, a systematic theory that allows both timed testing and timed refinement to be expressed. An important practical consequence is that this ensures that the notion of correctness used by developers guarantees that tests pass when applied to a correct system and, in addition, faults identified during testing correspond to development mistakes.

We present RoboSimVer, a tool for modeling and analyzing RoboSim models. It uses a graphical notation called RoboSim to describe platform-independent simulation models of robotic systems. For model analysis, we have implemented a model-transformation approach to translate RoboSim models into NTA (Network of Timed Automata) and their stochastic version based on patterns and mapping rules. RoboSimVer takes a RoboSim simulation model as input and provides different rigorous verification techniques to check whether the simulation models satisfy property constraints. For experimental demonstrations, we adopt the alpha algorithm for swarm robotics as a case study. We use an abstract robotic-platform model to describe a swarm in an uncertain environment and illustrate how our tool supports the verification of stochastic and hybrid systems. The demonstration video is at youtu.be/mNe4q64GkmQ.

Abstract Specifying budgets and deadlines using a process algebra like CSP requires an explicit notion of time. The tock-CSP encoding embeds a rich and flexible approach for modelling discrete-time behaviours with powerful tool support. It uses an event tock, interpreted to mark passage of time. Analysis, however, has traditionally used the standard semantics of CSP, which is inadequate for reasoning about timed refinement. The most recent version of the model checker FDR provides tailored support for tock-CSP, including specific operators, but the standard semantics remains inadequate. In this paper, we characterise tock-CSP as a language in its own right, rich enough to model budgets and deadlines, and reason about Zeno behaviour. We present the first sound tailored semantic model for tock-CSP that captures timewise refinement. It is fully mechanised in Isabelle/HOL and, to enable use of FDR4 to check refinement in this novel model, we use model shifting, which is a technique that explicitly encodes refusals in traces.

Abstract RoboChart is a timed domain-specific language for robotics, distinctive in its support for automated verification by model checking and theorem proving. Since uncertainty is an essential part of robotic systems, we present here an extension to RoboChart to model uncertainty using probabilism. The extension enriches RoboChart state machines with probability through a new construct: probabilistic junctions as the source of transitions with a probability value. RoboChart has an accompanying tool, called RoboTool, for modelling and verification of functional and real-time behaviour. We present here also an automatic technique, implemented in RoboTool, to transform a RoboChart model into a PRISM model for verification. We have extended the property language of RoboTool so that probabilistic properties expressed in temporal logic can be written using controlled natural language.

RoboSim is a tool-independent notation for modeling software simulations of robots, and it can be verified by a variety of techniques and tools, including model checking and theorem proving. RoboSim has a formal tock-CSP (Communicating Sequential Processes) semantics, and so refinement checkers, such as FDR, can be used for verification of models. In this paper, we explore the use of UPPAAL, as a well-established tool for verification of time-dependent properties. We propose a model-transformation strategy to translate RoboSim models into NTA (Network of Timed Automata) based on some patterns and mapping rules. We implement our strategy as a plug-in for the RoboSim modeling and verification tool. Using examples, we compare the verification results of UPPAAL and FDR for a series of safety, reachability, and liveness properties. Moreover, we use a robotic platform model of swarm robots in an uncertain environment, to illustrate how our approach can be extended to the verification of stochastic and hybrid systems using UPPAAL SMC. Such an extension cannot be easily conceived for The original tock-CSP semantics of RoboSim.

No abstract available.

No abstract available.

This article addresses refinement and testing based on CSP models, when we distinguish input and output events. In a testing experiment, the tester (or the environment) controls the inputs, and the system under test controls the outputs. The standard models and refinement relations of CSP, however, do not differentiate inputs and outputs and are not, therefore, entirely suitable for testing. Here, we consider an alphabet of events partitioned into inputs and outputs, and we present a novel refusal-testing model for CSP with a notion of input-output refusal-traces refinement. We compare that with the ioco relation often used in testing, and we find that it is more widely applicable and stronger. This means that mistakes found using traditional ioco testing do indicate mistakes in the development. Finally, we provide a CSP testing theory that takes into account inputs and outputs. With our theory, it becomes feasible to develop techniques and tools for automatic generation of realistic and sound tests from CSP models. Our work reconciles the normally disparate areas of refinement and (formal) testing by identifying how ioco testing can be used to inform refinement-based results and vice-versa.

No abstract available.

Robots are becoming ubiquitous: from vacuum cleaners to driverless cars, there is a wide variety of applications, many with potential safety hazards. The work presented in this paper proposes a set of constructs suitable for both modelling robotic applications and supporting verification via model checking and theorem proving. Our goal is to support roboticists in writing models and applying modern verification techniques using a language familiar to them. To that end, we present RoboChart, a domain-specific modelling language based on UML, but with a restricted set of constructs to enable a simplified semantics and automated reasoning. We present the RoboChart metamodel, its well-formedness rules, and its process-algebraic semantics. We discuss verification based on these foundations using an implementation of RoboChart and its semantics as a set of Eclipse plug-ins called RoboTool.

Mutation testing is a program-transformation technique that injects artificial bugs to check whether the existing test suite can detect them. However, the costs of using mutation testing are usually high, hindering its use in industry. Useless mutants (equivalent and duplicated) contribute to increase costs. Previous research has focused mainly on detecting useless mutants only after they are generated and compiled. In this paper, we introduce a strategy to help developers with deriving rules to avoid the generation of useless mutants. To use our strategy, we pass as input a set of programs. For each program, we also need a passing test suite and a set of mutants. As output, our strategy yields a set of useless mutants candidates. After manually confirming that the mutants classified by our strategy as "useless" are indeed useless, we derive rules that can avoid their generation and thus decrease costs. To the best of our knowledge, we introduce 37 new rules that can avoid useless mutants right before their generation. We then implement a subset of these rules in the MUJAVA mutation testing tool. Since our rules have been derived based on artificial and small Java programs, we take our MUJAVA version embedded with our rules and execute it in industrial-scale projects. Our rules reduced the number of mutants by almost 13% on average. Our results are promising because (i) we avoid useless mutants generation; (ii) our strategy can help with identifying more rules in case we set it to use more complex Java programs; and (iii) our MUJAVA version has only a subset of the rules we derived.

Robot software controllers are often concurrent and time critical, and requires modern engineering approaches for validation and verification. With this motivation, we have developed a tool and techniques for graphical modelling with support for automatic generation of underlying mathematical definitions for model checking. It is possible to check automatically both general properties, like absence of deadlock, and specific application properties. We cater both for timed and untimed modelling and verification. Our approach has been tried in examples used in a variety of robotic applications.

Summary Safety‐Critical Java (SCJ) is a profile of the Real‐Time Specification for Java that brings to the safety‐critical industry the possibility of using Java. SCJ defines three compliance levels: Level 0, Level 1 and Level 2. The SCJ specification is clear on what constitutes a Level 2 application in terms of its use of the defined API but not the occasions on which it should be used. This paper broadly classifies the features that are only available at Level 2 into three groups: nested mission sequencers, managed threads and global scheduling across multiple processors. We explore the first two groups to elicit programming requirements that they support. We identify several areas where the SCJ specification needs modifications to support these requirements fully; these include the following: support for terminating managed threads, the ability to set a deadline on the transition between missions and augmentation of the mission sequencer concept to support composibility of timing constraints. We also propose simplifications to the termination protocol of missions and their mission sequencers. To illustrate the benefit of our changes, we present excerpts from a formal model of SCJ Level 2 written inCircus, a state‐rich process algebra for refinement. Copyright © 2016 John Wiley & Sons, Ltd.

Context: The demand from industry for more dependable and scalable test-development mechanisms has fostered the use of formal models to guide the generation of tests.Despite many advancements having been obtained with state-based models, such as Finite State Machines (FSMs) and Input/Output Transition Systems (IOTSs), more advanced formalisms are required to specify large, state-rich, concurrent systems.Circus, a state-rich process algebra combining Z, CSP and a refinement calculus, is suitable for this; however, deriving tests from such models is accordingly more challenging.Recently, a testing theory has been stated for Circus, allowing the verification of process refinement based on exhaustive test sets.Objective: We investigate fault-based testing for refinement from Circus specifications using mutation.We seek the benefits of such techniques in test-set quality assertion and fault-based test-case selection.We target results relevant not only for Circus, but to any process algebra for refinement that combines CSP with a data language.Method: We present a formal definition for fault-based test sets, extending the Circus testing theory, and an extensive study of mutation operators for Circus.Using these results, we propose an approach to generate tests to kill mutants.Finally, we explain how prototype tool support can be obtained with the implementation of a mutant generator, a translator from Circus to CSP, and a refinement checker for CSP, and with a more sophisticated chain of tools that support the use of symbolic tests.Results: We formally characterise mutation testing for Circus, defining the exhaustive test sets that can kill a given mutant.We also provide a technique to select tests from these sets based on specification traces of the mutants.Finally, we present mutation operators that consider faults related to both reactive and data manipulation behaviour.Altogether, we define a new fault-based test-generation technique for Circus.Conclusion: We conclude that mutation testing for Circus can truly aid making test generation from state-rich model more tractable, by focussing on particular faults.

Safety-Critical Java (SCJ) is a version of Java suitable for programming real-time safety-critical systems; it is the result of an international standardisation effort to define a subset of the Real-Time Specification for Java (RTSJ). SCJ programs require the use of specialised virtual machines. We present here the result of our verification of the scheduler of the only SCJ virtual machine up to date with the standard and publicly available, the icecap HVM. We describe our approach for analysis of (SCJ) virtual machines, and illustrate it using the icecap HVM scheduler. Our work is based on a state-rich process algebra that combines Z and CSP, and we take advantage of well established tools.

CSP is well established as a process algebra for refinement. Most refinement relations for CSP do not differentiate between inputs and outputs, and so are unsuitable for testing. This paper provides CSP with a denotational semantics based on suspension traces; it gives the traditional CSP operators a novel view, catering for the differences between inputs and outputs. We identify healthiness conditions for the suspension-traces model and include a treatment of termination not contemplated in the context of input-output labelled transition systems. Using our suspension-traces semantics, we provide for CSP a characterisation of the conformance relation ioco, which is widely used in testing. Finally, we propose a strategy to mechanise the verification of conformance according to ioco and suspension-trace refinement using CSP tools. This work provides the basis for a theory of testing for CSP with inputs and outputs, and opens up the possibility of studying algebraic laws and compositional reasoning techniques based on ioco. Ultimately, it contributes to making CSP models useful for both design and testing of systems.

Abstract At the very beginning of system development, typically only natural-language requirements are documented. As an informal source of information, however, natural-language specifications may be ambiguous and incomplete; this can be hard to detect by means of manual inspection. In this work, we present a formal model, named data-flow reactive system (DFRS), which can be automatically obtained from natural-language requirements that describe functional, reactive and temporal properties. A DFRS can also be used to assess whether the requirements are consistent and complete. We define two variations of DFRS: a symbolic and an expanded version. A symbolic DFRS (s-DFRS) is a concise representation that inherently avoids an explicit representation of (possibly infinite) sets of states and, thus, the state space-explosion problem. We use s-DFRS as part of a technique for test-case generation from natural-language requirements. In our approach, an expanded DFRS (e-DFRS) is built dynamically from a symbolic one, possibly limited to some bound; in this way, bounded analysis (e.g., reachability, determinism, completeness) can be performed. We adopt the s-DFRS as an intermediary representation from which models, for instance, SCR and CSP, are obtained for the purpose of test generation. An e-DFRS can also be viewed as the semantics of the s-DFRS from which it is generated. In order to connect such a semantic representation to established ones in the literature, we show that an e-DFRS can be encoded as a TIOTS: an alternative timed model based on the widely used IOLTS and ioco. To validate our overall approach, we consider two toy examples and two examples from the aerospace and automotive industry. Test cases are independently created and we verify that they are all compatible with the corresponding e-DFRS models generated from symbolic ones. This verification is performed mechanically with the aid of the NAT2TEST tool, which supports the manipulation of such models.

Abstract Safety-Critical Java (SCJ) is a recent technology that changes the execution and memory model of Java in such a way that applications can be statically analysed and certified for their real-time properties and safe use of memory. Our interest is in the development of comprehensive and sound techniques for the formal specification, refinement, design, and implementation of SCJ programs, using a correct-by-construction approach. As part of this work, we present here an account of laws and patterns that are of general use for the refinement of SCJ mission specifications into designs of parallel handlers, as they are used in the SCJ programming paradigm. Our refinement notation is a combination of languages from theCircusfamily, supporting state-rich reactive models with the addition of class objects and real-time properties. Starting from a sequential and centralisedCircusspecification, our laws permit refinement intoCircusmodels of SCJ program designs. Automation and proof of the refinement laws is examined here, too. Our work is an important step towards eliciting laws of programming for SCJ and fits into a refinement strategy that we have developed previously to derive SCJ programs from specifications in a rigorous manner.

Theories for model-based testing identify exhaustive test sets: typically infinite sets of tests whose execution establishes the conformance relation of interest. Practical techniques rely on selection strategies to identify finite subsets of these tests, and popular approaches are based on requirements to cover the model. In previous work, we have defined testing theories for refinement-based process algebra, namely, CSP and Circus, a state-rich process algebra. In this paper, we consider the selection of tests designed to establish traces refinement. In this case, conformance does not require that all traces of the model are available in the system under test, and this can raise challenges regarding coverage criteria for selection. To address these difficulties, we present a framework for formalising a variety of selection strategies. We exemplify its use in the formalisation of a selection criterion based on coverage of process communications for integration testing. We consider models written in Circus, whose symbolic testing theory facilitates the definition of uniformity and regularity hypotheses based on data operations, but also imposes extra challenges for selection of concrete tests. Our results, however, are relevant for any formalism where the conformance relation does not require all the traces of the specification to be executable by the system under test.

Safety-critical Java (SCJ) is a restriction of the real-time specification for Java to support the development and certification of safety-critical applications. The SCJ technology specification is the result of an international effort from industry and academia. In this paper, we present a formalization of the SCJ Level 1 execution model, formalize a translation strategy from SCJ into a refinement notation and describe a tool that largely automates the generation of the formal models. Our modelling language is part of the Circus family; at the core, we have Z, communicating sequential processes and Morgan's calculus, but we also use object-oriented and timed constructs from the OhCircus and Circus Time variants. Our work is an essential ingredient for the development of refinement-based reasoning techniques for SCJ.

Abstract 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.

Abstract Simulink’s Stateflow is a graphical notation widely adopted in industry. Since it is frequently used to model safety-critical systems, correctness of implementations of Stateflow charts is a major concern. In previous work, we have shown how we can generate formal models for refinement of Stateflow charts automatically. Here, we define a refinement strategy that supports the automated verification of implementations with respect to these models. We consider the verification of implementations that follow architectural patterns used in the Stateflow code generator. We present a detailed procedure for application of refinement laws. If the implementation is correct, the procedure succeeds. If a law application fails, the implementation is either incorrect or does not use the expected architectural pattern. The very low proof burden associated with the refinement verification makes a high level of automation possible.

This paper addresses refinement and testing based on CSP models, when we distinguish input and output events. From a testing perspective, there is an asymmetry: the tester (or the environment) controls the inputs, and the system under test controls the outputs. The standard models and refinement relations of CSP are, therefore, not entirely suitable for testing. Here, we adapt the CSP stable-failures model, resulting in the notion of input-output failures refinement. We compare that with the ioco relation often used in testing.Finally, we adapt the CSP testing theory, and show that some tests become unnecessary. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Hoare and He's Unifying Theories of Programming (UTP) are a predicative relational framework for the definition and combination of refinement languages for a variety of programming paradigms. Previous work has defined a theory for angelic nondeterminism in the UTP; this is basically an encoding of binary multirelations in a predicative model. In the UTP a theory of designs (pre and postcondition pairs) provides, not only a model of terminating programs, but also a stepping stone to define a theory for state-rich reactive processes. In this paper, we cast the angelic nondeterminism theory of the UTP as a theory of designs with the long-term objective of providing a model for well established refinement process algebras like Communicating Sequential Processes (CSP) and Circus.

Abstract 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.

Abstract The increasing interest in the combination of different computational paradigms is well represented by Hoare and 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 and He’s unification, and for the mechanisation of languages whose semantics is based on the UTP.

Abstract ArcAngel is a tactic language devised to facilitate and automate program developments using Morgan’s refinement calculus. It is especially well suited for the specification of high-level refinement strategies, and equipped with a formal semantics that additionally permits reasoning about tactics. In this paper, we present an implementation of ArcAngel for the ProofPower theorem prover. We discuss the underlying design, explain how it implements the semantics of ArcAngel, and examine the interplay between ArcAngel tactics and the native reasoning support of the prover. We also discuss several extensions of ArcAngel that have been entailed by our implementation effort. They are of practical importance and provide a unification of the related tactic languages Angel and ArcAngelC. Our main result is a mechanisation that reflects directly the ArcAngel semantics, and can be used with any programming model for refinement. The approach can be used to support other formal tactic languages using other theorem provers.

Abstract Control engineers make extensive use of diagrammatic notations; control law diagrams are used in industry every day. Techniques and tools for analysis of these diagrams or their models are plentiful, but verification of their implementations is a challenge that has been taken up by few. We are aware only of approaches that rely on automatic code generation, which is not enough assurance for certification, and often not adequate when tailored hardware components are used. Our work is based onCircus, a notation that combines Z, CSP, and a refinement calculus, and on industrial tools that produce partial Z and CSP models of discrete-time Simulink diagrams. We present a strategy to translate Simulink diagrams toCircus, and a strategy to prove that a parallel Ada implementation refines theCircusspecification; we rely on aCircussemantics for the program. By using a combined notation, we provide a specification that considers both functional and behavioural aspects of a large set of diagrams, and support verification of a large number of implementations. We can handle, for instance, arbitrarily large data types and dynamic scheduling.

No abstract available.

Abstract In this paper we describe an algebraic approach to construct provably correct compilers for object-oriented languages; this is illustrated for programs written in a language similar to a sequential subset of Java. It includes recursive classes, inheritance, dynamic binding, recursion, type casts and test, assignment, and class-based visibility, but a copy semantics. In our approach, we tackle the problem of compiler correctness by reducing the task of compilation to that of program refinement. Compilation is identified with the reduction of a source program to a normal form that models the execution of object code. The normal form is generated by a series of correctness-preserving transformations that are proved sound from the basic laws of the language; therefore it is correct by construction. The main advantages of our approach are the characterisation of compilation within a uniform framework, where comparisons and translations between semantics are avoided, and the modularity and extensibility of the resulting compiler.

Abstract Following the trend to combine techniques to cover several facets of the development of modern systems, an integration of Z and CSP, calledCircus, has been proposed as a refinement language; its relational model, based on the unifying theories of programming (UTP), justifies refinement in the context of both Z and CSP. In this paper, we introduceCircus Time, a timed extension ofCircus, and present a new UTP time theory, which we use to give semantics toCircus Timeand to validate some of its laws. In addition, we provide a framework for validation of timed programs based on FDR, the CSP model-checker. In this technique, a syntactic transformation strategy is used to split a timed program into two parallel components: an untimed program that uses timer events, and a collection of timers. We show that, with the timer events, it is possible to reason about time properties in the untimed language, and so, using FDR. Soundness is established using a Galois connection between the untimed UTP theory ofCircus(and CSP) and our time theory.

Abstract 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.

No abstract available.

Abstract 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.

Abstract We present a refinement strategy for Circus , which is the combination of Z, CSP, and the refinement calculus in the setting of Hoare and 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.

Abstract. Morgan's refinement calculus is a successful technique for developing software in a precise and consistent way. This technique, however, can be hard to use, as developments may be long and repetitive. Many authors have pointed out that a lot can be gained by identifying commonly used development strategies, documenting them as tactics, and using them as single transformation rules. Also, it is useful to have a notation for describing derivations, so that they can be analysed and modified. In this paper, we present ArcAngel, a language for defining such refinement tactics; we present the language, its semantics, and some of its algebraic laws. Apart from Angel, a general-purpose tactic language that we are extending, no other tactic language has a denotational semantics and proof theory of its own.

This paper presents a formalisation of the steam boiler problem using Circus, a unified theory of the formal specification languages Z and CSP. The aim of Circus is to provide powerful support for the specification of the data-oriented and behavioural aspects of concurrent systems, and to provide a calculational development technique for languages similar to Occam, Java, and Handel-C.

We define a predicate-transformer semantics for an object oriented language that includes specification constructs from refinement calculi. The language includes recursive classes, visibility control, dynamic binding, and recursive methods. Using the semantics, we formulate notions of refinement. Such results are a first step toward a refinement calculus.

The lack of a method for developing programs from Z specifications is a widely recognized difficulty. In response to this problem, different approaches to the integration of Z with a refinement calculus have been proposed. These programming techniques are promising, but as far as we know, have not been formalized. Since they are based on refinement calculi formalized in terms of weakest preconditions, the definition of a weakest precondition semantics for Z is a significant contribution to the solution of this problem. In this paper, we actually construct a weakest precondition semantics from a relational semantics proposed by the Z standards panel. The construction provides reassurance as to the adequacy of the resulting semantics definition and additionally establishes an isomorphism between weakest preconditions and relations. Compositional formulations for the weakest precondition of some schema calculus expressions are provided.

Abstract. The fact that Z is a specification language only, with no associated program development method, is a widely recognised problem. As an answer to that, we present ZRC, a refinement calculus based on Morgan's work that incorporates the Z notation and follows its style and conventions. This work builds upon existing refinement techniques for Z, but distinguishes itself mainly in that ZRC is completely formalised. In this paper, we explain how programs can be derived from Z specifications using ZRC. We present ZRC-L, the language of our calculus, and its conversion laws, which are concerned with the transformation of Z schemas into programs of this language. Moreover, we present the weakest precondition semantics of ZRC-L, which is the basis for the derivation of the laws of ZRC. More than a refinement calculus, ZRC is a theory of refinement for Z.