-
Normative Requirements Operationalization with Large Language Models
Authors:
Nick Feng,
Lina Marsso,
S. Getir Yaman,
Isobel Standen,
Yesugen Baatartogtokh,
Reem Ayad,
Victória Oldemburgo de Mello,
Bev Townsend,
Hanne Bartels,
Ana Cavalcanti,
Radu Calinescu,
Marsha Chechik
Abstract:
Normative non-functional requirements specify constraints 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 chal…
▽ More
Normative non-functional requirements specify constraints 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 complementary 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 operationalization through a range of real-world case studies.
△ Less
Submitted 28 May, 2024; v1 submitted 18 April, 2024;
originally announced April 2024.
-
Creating a Digital Twin of Spinal Surgery: A Proof of Concept
Authors:
Jonas Hein,
Frédéric Giraud,
Lilian Calvet,
Alexander Schwarz,
Nicola Alessandro Cavalcanti,
Sergey Prokudin,
Mazda Farshad,
Siyu Tang,
Marc Pollefeys,
Fabio Carrillo,
Philipp Fürnstahl
Abstract:
Surgery digitalization is the process of creating a virtual replica of real-world surgery, also referred to as a surgical digital twin (SDT). It has significant applications in various fields such as education and training, surgical planning, and automation of surgical tasks. In addition, SDTs are an ideal foundation for machine learning methods, enabling the automatic generation of training data.…
▽ More
Surgery digitalization is the process of creating a virtual replica of real-world surgery, also referred to as a surgical digital twin (SDT). It has significant applications in various fields such as education and training, surgical planning, and automation of surgical tasks. In addition, SDTs are an ideal foundation for machine learning methods, enabling the automatic generation of training data. In this paper, we present a proof of concept (PoC) for surgery digitalization that is applied to an ex-vivo spinal surgery. The proposed digitalization focuses on the acquisition and modelling of the geometry and appearance of the entire surgical scene. We employ five RGB-D cameras for dynamic 3D reconstruction of the surgeon, a high-end camera for 3D reconstruction of the anatomy, an infrared stereo camera for surgical instrument tracking, and a laser scanner for 3D reconstruction of the operating room and data fusion. We justify the proposed methodology, discuss the challenges faced and further extensions of our prototype. While our PoC partially relies on manual data curation, its high quality and great potential motivate the development of automated methods for the creation of SDTs.
△ Less
Submitted 22 May, 2024; v1 submitted 25 March, 2024;
originally announced March 2024.
-
Domain adaptation strategies for 3D reconstruction of the lumbar spine using real fluoroscopy data
Authors:
Sascha Jecklin,
Youyang Shen,
Amandine Gout,
Daniel Suter,
Lilian Calvet,
Lukas Zingg,
Jennifer Straub,
Nicola Alessandro Cavalcanti,
Mazda Farshad,
Philipp Fürnstahl,
Hooman Esfandiari
Abstract:
This study tackles key obstacles in adopting surgical navigation in orthopedic surgeries, including time, cost, radiation, and workflow integration challenges. Recently, our work X23D showed an approach for generating 3D anatomical models of the spine from only a few intraoperative fluoroscopic images. This negates the need for conventional registration-based surgical navigation by creating a dire…
▽ More
This study tackles key obstacles in adopting surgical navigation in orthopedic surgeries, including time, cost, radiation, and workflow integration challenges. Recently, our work X23D showed an approach for generating 3D anatomical models of the spine from only a few intraoperative fluoroscopic images. This negates the need for conventional registration-based surgical navigation by creating a direct intraoperative 3D reconstruction of the anatomy. Despite these strides, the practical application of X23D has been limited by a domain gap between synthetic training data and real intraoperative images.
In response, we devised a novel data collection protocol for a paired dataset consisting of synthetic and real fluoroscopic images from the same perspectives. Utilizing this dataset, we refined our deep learning model via transfer learning, effectively bridging the domain gap between synthetic and real X-ray data. A novel style transfer mechanism also allows us to convert real X-rays to mirror the synthetic domain, enabling our in-silico-trained X23D model to achieve high accuracy in real-world settings.
Our results demonstrated that the refined model can rapidly generate accurate 3D reconstructions of the entire lumbar spine from as few as three intraoperative fluoroscopic shots. It achieved an 84% F1 score, matching the accuracy of our previous synthetic data-based research. Additionally, with a computational time of only 81.1 ms, our approach provides real-time capabilities essential for surgery integration.
Through examining ideal imaging setups and view angle dependencies, we've further confirmed our system's practicality and dependability in clinical settings. Our research marks a significant step forward in intraoperative 3D reconstruction, offering enhancements to surgical planning, navigation, and robotics.
△ Less
Submitted 18 June, 2024; v1 submitted 29 January, 2024;
originally announced January 2024.
-
Analyzing and Debugging Normative Requirements via Satisfiability Checking
Authors:
Nick Feng,
Lina Marsso,
Sinem Getir Yaman,
Yesugen Baatartogtokh,
Reem Ayad,
Victória Oldemburgo de Mello,
Beverley Townsend,
Isobel Standen,
Ioannis Stefanakos,
Calum Imrie,
Genaína Nunes Rodrigues,
Ana Cavalcanti,
Radu Calinescu,
Marsha Chechik
Abstract:
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…
▽ More
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 challenge, 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 (WFI), such as conflicts, redundancy, restrictiveness, insufficiency, yielding diagnostics which 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 ranging from assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.
△ Less
Submitted 11 January, 2024;
originally announced January 2024.
-
Specification, Validation and Verification of Social, Legal, Ethical, Empathetic and Cultural Requirements for Autonomous Agents
Authors:
Sinem Getir Yaman,
Ana Cavalcanti,
Radu Calinescu,
Colin Paterson,
Pedro Ribeiro,
Beverley Townsend
Abstract:
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 verif…
▽ More
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.
△ Less
Submitted 7 July, 2023;
originally announced July 2023.
-
Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata
Authors:
Abdulrazaq Abba,
Ana Cavalcanti,
Jeremy Jacob
Abstract:
In this work, we consider translating tock-CSP into Timed Automata for UPPAAL to facilitate using UPPAAL in reasoning about temporal specifications of tock-CSP models. The process algebra tock-CSP provides textual notations for modelling discrete-time behaviours, with the support of tools for automatic verification. Similarly, automatic verification of Timed Automata (TA) with a graphical notation…
▽ More
In this work, we consider translating tock-CSP into Timed Automata for UPPAAL to facilitate using UPPAAL in reasoning about temporal specifications of tock-CSP models. The process algebra tock-CSP provides textual notations for modelling discrete-time behaviours, with the support of tools for automatic verification. Similarly, automatic verification of Timed Automata (TA) with a graphical notation is supported by the UPPAAL real-time verification toolbox \uppaal. The two modelling approaches, TA and tock-CSP, differ in both modelling and verification approaches, temporal logic and refinement, respectively, as well as their provided facilities for automatic verification. For instance, liveness requirements are difficult to specify with the constructs of tock-CSP, but they are easy to specify and verify in UPPAAL. To take advantage of temporal logic, we translate tock-CSP into TA for \uppaal; we have developed a translation technique and its supporting tool. We provide rules for translating tock-CSP into a network of small TAs for capturing the compositional structure of tock-CSP that is not available in TA. For validation, we start with an experimental approach based on finite approximations to trace sets. Then, we explore mathematical proof to establish the correctness of the rules for covering infinite traces.
△ Less
Submitted 27 April, 2021;
originally announced April 2021.
-
Automatic Translation of tock-CSP into Timed Automata
Authors:
Abdulrazaq Abba,
Ana Cavalcanti,
Jeremy Jacob
Abstract:
The process algebra tock-CSP provides textual notations for modelling discrete-time behaviours, with the support of various tools for verification. Similarly, automatic verification of Timed Automata (TA) is supported by the real-time verification toolbox UPPAAL. TA and tock-CSP differ in both modelling and verification approaches. For instance, liveness requirements are difficult to specify with…
▽ More
The process algebra tock-CSP provides textual notations for modelling discrete-time behaviours, with the support of various tools for verification. Similarly, automatic verification of Timed Automata (TA) is supported by the real-time verification toolbox UPPAAL. TA and tock-CSP differ in both modelling and verification approaches. For instance, liveness requirements are difficult to specify with the constructs of tock-CSP, but they are easy to verify in UPPAAL. In this work, we translate tock-CSP into TA to take advantage of UPPAAL. We have developed a translation technique and tool; our work uses rules for translating tock-CSP into a network of small TA, which address the complexity of capturing the compositionality of tock-CSP . For validation, we use an experimental approach based on finite approximations to trace sets. We plan to use mathematical proof to establish the correctness of the rules that will cover an infinite set of traces.
△ Less
Submitted 29 April, 2021; v1 submitted 16 August, 2020;
originally announced August 2020.
-
Automated Verification of Reactive and Concurrent Programs by Calculation
Authors:
Simon Foster,
Kangfeng Ye,
Ana Cavalcanti,
Jim Woodcock
Abstract:
Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber-physical systems and autonomous robots. In this paper, we present an algebraic verification strategy for concurrent reactive programs, with a large or infin…
▽ More
Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber-physical systems and autonomous robots. In this paper, we present an algebraic verification strategy for concurrent reactive programs, with a large or infinite state space. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, based on Kleene algebra, and for parallel composition. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He's Unifying Theories of Programming (UTP) framework, to provide soundness guarantees and practical verification support.
△ Less
Submitted 12 April, 2021; v1 submitted 27 July, 2020;
originally announced July 2020.
-
Priorities in tock-CSP
Authors:
Pedro Ribeiro,
James Baxter,
Ana Cavalcanti
Abstract:
The $tock$-CSP encoding embeds a rich and flexible approach to modelling discrete timed behaviours in CSP where the event $tock$ is interpreted to mark the passage of time. The model checker FDR provides tailored support for $tock$-CSP, including a prioritisation operator that has typically been used to ensure maximal progress, where time only advances after internal activity has stabilised. Prior…
▽ More
The $tock$-CSP encoding embeds a rich and flexible approach to modelling discrete timed behaviours in CSP where the event $tock$ is interpreted to mark the passage of time. The model checker FDR provides tailored support for $tock$-CSP, including a prioritisation operator that has typically been used to ensure maximal progress, where time only advances after internal activity has stabilised. Prioritisation may also be used on its own right as a modelling construct. Its operational semantics, however, is only congruent over the most discriminating semantic model of CSP: the finite-linear model. To enable sound and compositional reasoning in a $tock$-CSP setting, we calculate a denotational definition for prioritisation. For that we establish a Galois connection between a specialisation of the finite-linear model, with $tock$ and $\checkmark$, that signals termination, as special events, and $\checkmark$-$tock$-CSP, a model for $tock$-CSP that captures termination, deadlines, and is adequate for reasoning about timed refinement. Our results are mechanised using Isabelle/HOL.
△ Less
Submitted 18 July, 2019;
originally announced July 2019.
-
Unifying Semantic Foundations for Automated Verification Tools in Isabelle/UTP
Authors:
Simon Foster,
James Baxter,
Ana Cavalcanti,
Jim Woodcock,
Frank Zeyda
Abstract:
The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration relies on unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is…
▽ More
The growing complexity and diversity of models used in the engineering of dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration relies on unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He's Unifying Theories of Programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories for diverse paradigms, and their use in constructing formalised semantic models. These can be further applied in the development of verification tools, harnessing Isabelle's proof automation facilities. Several layers of mathematical foundations are developed, including lenses to model variables and state spaces as algebraic objects, alphabetised predicates and relations to model programs, including algebraic and axiomatic semantics, proof tools for Hoare logic and refinement calculus, and UTP theories to encode computational paradigms.
△ Less
Submitted 22 June, 2020; v1 submitted 14 May, 2019;
originally announced May 2019.
-
Automating Verification of State Machines with Reactive Designs and Isabelle/UTP
Authors:
Simon Foster,
James Baxter,
Ana Cavalcanti,
Alvaro Miyazawa,
Jim Woodcock
Abstract:
State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal verification techniques are important, and can be cost-effective if they are both automated and scalable. In this paper, we present a verification approach for a diagrammatic state machine language that utilises theorem p…
▽ More
State-machine based notations are ubiquitous in the description of component systems, particularly in the robotic domain. To ensure these systems are safe and predictable, formal verification techniques are important, and can be cost-effective if they are both automated and scalable. In this paper, we present a verification approach for a diagrammatic state machine language that utilises theorem proving and a denotational semantics based on Unifying Theories of Programming (UTP). We provide the necessary theory to underpin state machines (including induction theorems for iterative processes), mechanise an action language for states and transitions, and use these to formalise the semantics. We then describe the verification approach, which supports infinite state systems, and exemplify it with a fully automated deadlock-freedom check. The work has been mechanised in our proof tool, Isabelle/UTP, and so also illustrates the use of UTP to build practical verification tools.
△ Less
Submitted 24 August, 2018; v1 submitted 23 July, 2018;
originally announced July 2018.
-
Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra
Authors:
Simon Foster,
Kangfeng Ye,
Ana Cavalcanti,
Jim Woodcock
Abstract:
Reactive programs are ubiquitous in modern applications, and so verification is highly desirable. We present a verification strategy for reactive programs with a large or infinite state space utilising algebraic laws for reactive relations. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's…
▽ More
Reactive programs are ubiquitous in modern applications, and so verification is highly desirable. We present a verification strategy for reactive programs with a large or infinite state space utilising algebraic laws for reactive relations. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, which is supported by Kleene algebra. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, which provides soundness guarantees, and practical verification support.
△ Less
Submitted 7 August, 2018; v1 submitted 6 June, 2018;
originally announced June 2018.
-
A Formal Model of the Safety-Critical Java Level 2 Paradigm
Authors:
Matt Luckcuck,
Ana Cavalcanti,
Andy Wellings
Abstract:
Safety-Critical Java (SCJ) introduces a new programming paradigm for applications that must be certified. The SCJ specification (JSR 302) is an Open Group Standard, but it does not include verification techniques. Previous work has addressed verification for SCJ Level~1 programs. We support the much more complex SCJ Level~2 programs, which allows the programming of highly concurrent multi-processo…
▽ More
Safety-Critical Java (SCJ) introduces a new programming paradigm for applications that must be certified. The SCJ specification (JSR 302) is an Open Group Standard, but it does not include verification techniques. Previous work has addressed verification for SCJ Level~1 programs. We support the much more complex SCJ Level~2 programs, which allows the programming of highly concurrent multi-processor applications with Java threads, and wait and notify mechanisms. We present a formal model of SCJ Level~2 that captures the state and behaviour of both SCJ programs and the SCJ API. This is the first formal semantics of the SCJ Level~2 paradigm and is an essential ingredient in the development of refinement-based reasoning techniques for SCJ Level~2 programs. We show how our models can be used to prove properties of the SCJ API and applications.
△ Less
Submitted 27 May, 2018;
originally announced May 2018.
-
Safety-Critical Java: Level 2 in Practice
Authors:
Matt Luckcuck,
Andy Wellings,
Ana Cavalcanti
Abstract:
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 broa…
▽ More
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:~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 in Circus, a state-rich process algebra for refinement.
△ Less
Submitted 27 May, 2018;
originally announced May 2018.
-
Unifying Theories of Reactive Design Contracts
Authors:
Simon Foster,
Ana Cavalcanti,
Samuel Canham,
Jim Woodcock,
Frank Zeyda
Abstract:
Design-by-contract is an important technique for model-based design in which a composite system is specified by a collection of contracts that specify the behavioural assumptions and guarantees of each component. In this paper, we describe a unifying theory for reactive design contracts that provides the basis for modelling and verification of reactive systems. We provide a language for expression…
▽ More
Design-by-contract is an important technique for model-based design in which a composite system is specified by a collection of contracts that specify the behavioural assumptions and guarantees of each component. In this paper, we describe a unifying theory for reactive design contracts that provides the basis for modelling and verification of reactive systems. We provide a language for expression and composition of contracts that is supported by a rich calculational theory. In contrast with other semantic models in the literature, our theory of contracts allow us to specify both the evolution of state variables and the permissible interactions with the environment. Moreover, our model of interaction is abstract, and supports, for instance, discrete time, continuous time, and hybrid computational models. Being based in Unifying Theories of Programming (UTP), our theory can be composed with further computational theories to support semantics for multi-paradigm languages. Practical reasoning support is provided via our proof framework, Isabelle/UTP, including a proof tactic that reduces a conjecture about a reactive program to three predicates, symbolically characterising its assumptions and guarantees about intermediate and final observations. This allows us to verify programs with a large or infinite state space. Our work advances the state-of-the-art in semantics for reactive languages, description of their contractual specifications, and compositional verification.
△ Less
Submitted 9 September, 2019; v1 submitted 29 December, 2017;
originally announced December 2017.
-
Unifying Theories of Time with Generalised Reactive Processes
Authors:
Simon Foster,
Ana Cavalcanti,
Jim Woodcock,
Frank Zeyda
Abstract:
Hoare and He's theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. In this paper, we show how their theory can be generalised by using an abstract trace algebra. We show how the algebra, notably, allows us to also…
▽ More
Hoare and He's theory of reactive processes provides a unifying foundation for the formal semantics of concurrent and reactive languages. Though highly applicable, their theory is limited to models that can express event histories as discrete sequences. In this paper, we show how their theory can be generalised by using an abstract trace algebra. We show how the algebra, notably, allows us to also consider continuous-time traces and thereby facilitate models of hybrid systems. We then use this algebra to reconstruct the theory of reactive processes in our generic setting, and prove characteristic laws for sequential and parallel processes, all of which have been mechanically verified in the Isabelle/HOL proof assistant.
△ Less
Submitted 21 February, 2018; v1 submitted 29 December, 2017;
originally announced December 2017.
-
From Formalised State Machines to Implementations of Robotic Controllers
Authors:
Wei Li,
Alvaro Miyazawa,
Pedro Ribeiro,
Ana Cavalcanti,
Jim Woodcock,
Jon Timmis
Abstract:
Controllers for autonomous robotic systems can be specified using state machines. However, these are typically developed in an ad hoc manner without formal semantics, which makes it difficult to analyse the controller. Simulations are often used during the development, but a rigorous connection between the designed controller and the implementation is often overlooked. This paper presents a state-…
▽ More
Controllers for autonomous robotic systems can be specified using state machines. However, these are typically developed in an ad hoc manner without formal semantics, which makes it difficult to analyse the controller. Simulations are often used during the development, but a rigorous connection between the designed controller and the implementation is often overlooked. This paper presents a state-machine based notation, RoboChart, together with a tool to automatically create code from the state machines, establishing a rigorous connection between specification and implementation. In RoboChart, a robot's controller is specified either graphically or using a textual description language. The controller code for simulation is automatically generated through a direct map** from the specification. We demonstrate our approach using two case studies (self-organized aggregation and swarm taxis) in swarm robotics. The simulations are presented using two different simulators showing the general applicability of our approach.
△ Less
Submitted 6 February, 2017;
originally announced February 2017.
-
SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java
Authors:
Alvaro Miyazawa,
Ana Cavalcanti
Abstract:
Safety-Critical Java (SCJ) is a version of Java whose goal is to support the development of real-time, embedded, safety-critical software. In particular, SCJ supports certification of such software by introducing abstractions that enforce a simpler architecture, and simpler concurrency and memory models. In this paper, we present SCJ-Circus, a refinement-oriented formal notation that supports the…
▽ More
Safety-Critical Java (SCJ) is a version of Java whose goal is to support the development of real-time, embedded, safety-critical software. In particular, SCJ supports certification of such software by introducing abstractions that enforce a simpler architecture, and simpler concurrency and memory models. In this paper, we present SCJ-Circus, a refinement-oriented formal notation that supports the specification and verification of low-level programming models that include the new abstractions introduced by SCJ. SCJ-Circus is part of the family of state-rich process algebra Circus, as such, SCJ-Circus includes the Circus constructs for modelling sequential and concurrent behaviour, real-time and object orientation. We present here the syntax and semantics of SCJ-Circus, which is defined by map** SCJ-Circus constructs to those of standard Circus. This is based on an existing approach for modelling SCJ programs. We also extend an existing Circus-based refinement strategy that targets SCJ programs to account for the generation of SCJ-Circus models close to implementations in SCJ.
△ Less
Submitted 7 June, 2016;
originally announced June 2016.
-
Refining SCJ Mission Specifications into Parallel Handler Designs
Authors:
Frank Zeyda,
Ana Cavalcanti
Abstract:
Safety-Critical Java (SCJ) is a recent technology that restricts 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 c…
▽ More
Safety-Critical Java (SCJ) is a recent technology that restricts 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 used in the SCJ programming paradigm. Our notation is a combination of languages from the Circus family, supporting state-rich reactive models with the addition of class objects and real-time properties. Our work is a first step to elicit laws of programming for SCJ and fits into a refinement strategy that we have developed previously to derive SCJ programs.
△ Less
Submitted 27 May, 2013;
originally announced May 2013.
-
Refinement-based verification of sequential implementations of Stateflow charts
Authors:
Alvaro Miyazawa,
Ana Cavalcanti
Abstract:
Simulink/Stateflow charts are widely used in industry for the specification of control systems, which are often safety-critical. This suggests a need for a formal treatment of such models. In previous work, we have proposed a technique for automatic generation of formal models of Stateflow blocks to support refinement-based reasoning. In this article, we present a refinement strategy that supports…
▽ More
Simulink/Stateflow charts are widely used in industry for the specification of control systems, which are often safety-critical. This suggests a need for a formal treatment of such models. In previous work, we have proposed a technique for automatic generation of formal models of Stateflow blocks to support refinement-based reasoning. In this article, we present a refinement strategy that supports the verification of automatically generated sequential C implementations of Stateflow charts. In particular, we discuss how this strategy can be specialised to take advantage of architectural features in order to allow a higher level of automation.
△ Less
Submitted 21 June, 2011;
originally announced June 2011.
