This work follow the verification as planning paradigm and propose to use model-checking techniques to solve planning and goal reasoning problems for autonomous systems with high-degree of assurance. It presents a novel modelling framework — Goal Task Network (GTN) that encompass both goal reasoning and planning under a unified formal description that enables the use of assurance tools. The paper provides a systematic method that highlights how an industrial model checker (PAT) can be used to solve goal reasoning and planning problems modelled by GTNs. Further, this paper also introduces the design of an automated system framework for Goal Reasoning And Verification for Independent Trusted Autonomous Systems (GRAVITAS). The proposed framework is demonstrated in an experiment that simulates a survey mission performed by the REMUS-100 autonomous underwater vehicle.

Reflection is a notion that naturally emerges from philosophy, mathematics, and sciences. In short, reflection is the ability of an entity to alter its own behaviour. This paper suggests that reflection is crucial to the development of complex and trustworthy software systems. We present RL, a reflective computational model that aims to support the development of a large-scale framework for modelling and manipulating structured data. We give the formal semantics for this computational model. We also share preliminary work on a proof-of-concept implementation of RL and discuss future work.

The design of embedded and hybrid systems requires powerful mechanisms for modeling data, state, concurrency and real-time behaviour. The {first} part of this paper illustrates a powerful design notation Timed Communicating Object Z (TCOZ) that has both channel based and sensor/actuator based interfaces. We believe that TCOZ is well suited for presenting more complete and coherent design models for complex embedded and hybrid systems. However, the challenge is how to analyze and check these models with tools support. One effective approach is to project (transform) the design models into multiple domains, then to use existing specialized tools in those domains to perform the checking and analyzing tasks. The second part of this paper demonstrates one particular projection from TCOZ designs to Timed Automata (TA) models so that TA model checkers can be used to check time related properties.

Semantic Web is regarded as the next generation of the World Wide Web. It provides not only the structure of the Web but also meaningful semantics for the information presented. To make semantic Web services understandable for distributed agents, formal definitions of the ontologies and their consistencies are essential. However, the existing tools for reasoning about semantic Web ontologies are still primitive. We believe that mature software engineering tools, such as theorem provers, can contribute to the reasoning phase. In this paper, we present an approach of encoding the semantic Web ontology (DAML+OIL) into the generic theorem prover Isabelle/HOL for automatic reasoning. Furthermore, a translation tool was developed to transform semantic Web ontologies into their extended Isabelle theories. With additional intermediate lemmas, Isabelle can be used to perform both subsumption (class) level and instantiation (instance) level reasoning of the semantic Web ontologies.

Abstract. Formal methods can be used in effective combination only if the semantic links between individual methods are clearly established. This paper discusses the semantic design of TCOZ, a language blended from Object-Z and TCSP. The semantic model adopted is the infinite timed failures model of TCSP, extended to include initial state and update events for modelling operations on internal state. An infinite trace model has been used so as to ensure proper account is taken of the potentially unbounded non-determinism allowed by Z schemas.

This paper describes a timed, multithreaded object modeling notation for specifying real-time, concurrent, and reactive systems. The notation Timed Communicating Object Z (TCOZ) builds on Object Z's strengths in modeling complex data and algorithms, and on Timed CSP's strengths in modeling process control and real-time interactions. TCOZ Is novel in that it includes timing primitives, properly separates process control and data/algorithm issues and supports the modeling of true multithreaded concurrency. TCOZ is particularly well-suited for specifying complex systems whose components have their own thread of control. The expressiveness of the notation is demonstrated by a case study in specifying a multilift system that operates in real-time.

Safety critical systems, such as aviation systems controlled by software, often have hard real-time requirements. Producing the correct result at the right time is the fundamental goal of such systems. Formally specifying the system functions and the timing requirements is the crucial step towards achieving such a goal. Aviation systems often need to be modified or upgraded on a regular basis, i.e. functionality and timing constraints may be altered. Therefore, the formal specification of such systems needs to be easily reused, maintained and modified. This paper demonstrates how the task scheduling aspects of an aircraft mission computer can be formalised in TCOZ.

Abstract. A syntactic calculation of Morgan's least conjunctive refinement operator for predicate transformers is developed. The operator is used to develop a general approach to lifting relational operators to predicate transformer operators. Predicate transformer versions of the relational conjunction and disjunction operators are considered in detail. The Z-based technique of program promotion is considered in a refinement calculus setting. A standard Z promotion example is recast in the refinement calculus.

Active objects have their own thread of control and passive objects are controlled by others. In Object-Z, all objects are modelled as passive objects. Timed Communicating Object Z (TCOZ) extends the Object-Z notation with Timed CSP's process and timing constructs. The blending of the concepts of object and non-terminating process leads to the notion of active object in TCOZ. This paper considers the concept of active object, its role and implications in formal real-time object-oriented specification.

We show how familiar mathematical concepts from differential and integral calculus can be represented in the Z specification language. Digital computer systems involve hardware devices and software variables that can adopt a limited range of values only, and may be temporarily inaccessible or ill-defined. Emphasis is therefore given to supporting discrete range types and partial functions.

Object-Z is an extension to the Z language designed to facilitate specification in an object-oriented style. It is an excellent tool for modeling data and algorithms, but its object semantics are single threaded and operations are atomic. Therefore, it is difficult to use Object-Z to capture the behaviour of concurrent real-time reactive systems. On the other hand, Timed CSP is good at modeling real-time concurrent behaviour, but has little support for modeling the state of a complex system. This paper introduces a blending of Object-Z and Timed CSP, known as TCOZ. The blended notation is particularly suited for specifying complex systems whose components have their own thread of control.

Abstract In the physical sciences and engineering, units of measurement provide a valuable aid to both the exposition and comprehension of physical systems. In addition, they provide an error checking facility comparable to static type checking commonly found with programming languages. It is argued that units of measurement can provide similar benefits in the specification and design of software and computer systems. To demonstrate this, we present an extension of the Z specification notation with support for the incorporation of units in specifications and demonstrate the feasibility of static dimensional analysis of the resulting language.

A specification and top-level refinement of a simple mine pump control system, as well as a proof of correctness of the refinement, are presented as an example of the application of a formal method for the development of time-based systems. The overall approach makes use of a refinement calculus for timed systems, similar to the refinement calculi for sequential programs. The specification makes use of topologically continuous functions of time to describe both analog and discrete properties of both the system and its refinements. The basic building block of specifications is a specification statement that gives a clear separation between the specification of the assumptions that the system may make about the environment in which it is to be placed, and the effect the system is guaranteed to achieve if placed in such an environment. The top-level refinement of the system is developed by application of refinement laws that allow design decisions to be made, local state to be introduced, and the decomposition of systems into pipelined and/or parallel processes.>