“FM in NZ” was the result of several happy coincidences. Martin Henson (University of Essex) was making one of his (approximately) annual visits to Steve Reeves and the rest of the FM group at Waikato, so we invited Lindsay Groves and Ray Nickson (Victoria University of Wellington) up to visit. Though Ray was not able to come at short notice, Lindsay was, so we booked him in for a departmental seminar.
Then, out of the blue, an email from Jing Sun at Auckland (who had visited us before) said that Jin Song Dong (his PhD supervisor) was going to be visiting him from Singapore. Many of us know Jin Song from various conferences (and Mark Utting and Petra Malik here at Waikato are working with him on the CZT project) so, of course, we invited Jing and Jin Song to the day too.
At the time we happened also to have Ali Pouyan from Birjand University in Iran and Rohit Bansal from IIT in New Delhi in India visiting, so this was a truly multi-national day and too good a chance to miss getting everyone together, which we managed to do at extremely short notice. Thanks to everyone for their patience and flexibility!Steve Reeves
Formal specification allows us to design and model the behaviour of computer systems and test their correctness prior to implementation. For any sort of computer system, the problem of being sure you've asked for the right thing (validating the specification against the user's requirements) and then being sure you're implementing the right thing (verifying the implementation relative to the specification) are important and hard problems. If the system also has a user interface, which is true in the majority of cases, there are the analogous additional problems of making sure that the interface allows any interaction that is required, and works in a usable way. HCI design guidelines are used in both design and evaluation of user interfaces to try and ensure that the systems we build are usable. This project aims to use formal methods to model guidelines for interface design then use these as a basis for the formal proof of the usability of a specified system.
Research on features has received much attention in the software engineering community. However, the representation and analysis of feature models are still largely informal. There is also an increasing need for methods and tools that can support feature model analysis. This talk presents an approach to formalizing and analyzing feature models using the Alloy constraint language. A formal semantics for the feature modeling language is defined in Alloy. The defined feature semantics provides a precise and rigorous formal basis for the structural analysis of feature models. Furthermore, we demonstrate that the consistency of a feature model and its configurations can be automatically checked by the Alloy Analyzer. A case study of the Graph Product Line (GPL) feature model is presented to illustrate the feature model analyzing process.
Jin Song Dong
(Based on an ICFEM'04 paper)
The integrated logic-based modelling language, Timed Communicating Object Z (TCOZ), is well suited for presenting more complete and coherent requirement models for complex real-time systems. However, the challenge is how to verify the TCOZ models with tool support, especially for analyzing timing properties. Graph-based modelling technique, Timed Automata (TA), has powerful mechanisms for designing real-time models using multiple clocks and has well developed automatic tool support. One weakness of TA is the lack of high-level composable graphical patterns to support the systematic design for complex systems. The investigation of the possible links between TCOZ and TA may benefit both techniques. For TCOZ, TA's tool support can be reused to check timing properties (rather than developing a new TCOZ tool from scratch). For TA, a set of composable graphical patterns can be defined based on the semantics of the TCOZ constructs, so that those patterns can be reused in a generic way. This paper firstly defines the composable TA graphical patterns, then presents sound transformation rules and a tool for projecting TCOZ specifications into TA. A case study of a railcar system is demonstrated.
Jin Song Dong
(Based on an ICSE'04 tutorial)
Following the success of XML, W3C envisions the Semantic Web (SW) as the next generation of web in which data are given well-defined and machine-understandable semantics so that they can be processed by intelligent software agents. SW can be regarded as an emerging area from the Knowledge Representation and the Web Communities. The formal methods community can also play an important role in the SW development. Modelling and verification techniques can be useful at many stages during the design, maintenance and deployment of SW ontology. We believe SW will be a new research and application domain for formal modeling techniques and tools. For example, recent research results have shown that Z and Alloy can provide modeling, reasoning and consistency checking services for SW. The talk will and present latest research investigations on Formal Methods for Semantic Web.
Slides covering both talks (PDF)
(Joint work with Simon Doherty, Victoria University, and Mark Moir and Victor Luchangco, Sun Microsystems Laboratories, Boston.)
Lock-free implementations of concurrent data structures have been developed to overcome problems associated with the use of the traditional locking techniques, which render them impractical in large scale concurrent environments. Although they offer considerable performance improvements, lock-free algorithms are typically quite subtle and many of the published algorithms are incorrect—even ones accompanied by ``proofs'' of correctness. There is therefore a need to develop more rigorous techniques for verifying such algorithms.
This talk will describe one of the most widely used lock-free algorithms: Michael and Scott's lock-free FIFO queue implementation, showing informally how it works. It will then present an overview of a semi-automated formal verification of a slightly optimised version of the algorithm. We verify the algorithm by proving a simulation relation between an automaton modelling the algorithm and one modelling the behaviour of a FIFO queue. An interesting aspect of the proof is that it requires a combination of two simulations: a forward simulation from the implementation automaton to an intermediate automaton, and a backward simulation from the intermediate automaton to the specification automaton. These automata are encoded in the input language of the PVS proof system, and the properties needed to show that the algorithm implements the specification are proved using PVS's theorem prover.
µCharts is a simplified StateCharts-like language for specifying the behaviour of reactive systems. While it is typical to give the semantics of such a language based on traces of observable behaviour, we have given µCharts a partial-correctness semantics using Z as a meta-language. Given this definition, a refinement calculus for charts has also been developed based on the "usual" notion of refinement for Z. As with any language that includes operators allowing specifications to be written in a structured manner, the monotonicity properties of these operators are important. By monotonicity we mean that a refinement of one part of a specification results in a refinement of the specification as a whole. Thus allowing piece-wise formal development of systems from specifications. We will demonstrate the side-conditions necessary in order that chart refinement is monotonic over the composition operator.
Our Causal Process Algebra (CPA) is based on two sets of observable actions: the active or causal set of actions and the passive or reactive set of actions. In addition we will add priority to the actions and when two t actions are possible then the t action with the highest priority will be executed.
Using this model we are able to: extend the situation in which incremental design by refinement is applicable; define determinism so that it is preserved by parallel composition with private and exclusive communication (Milner's restrictive composition); and we claim that small deterministic processes in our model are implementable whereas they are not for process algebras like CSP and CCS.
The framework nZ is a radical modification of the specification language Z. The differences are as follows:
Z is based on a partial-correctness semantics: nZ is based on a total-correctness semantics;
Z identifies chaos and magic (blocking): nZ distinguishes between these;
Z schema operators are not monotonic: nZ schema operators are all monotonic;
Z is based on equality: nZ is based on refinement;
Z is a specification language: nZ is wide-spectrum, integrating a programming language;
Z is relatively inflexible: nZ is extensible;
Z is a language: nZ is a logic;
I will concentrate on showing how nZ can be used to specify, internally, recursive procedures over arbitrary free-types, and the refinement logic that this induces.
Existing Logic Controller (LC) design methods, including Ladder Logic Diagrams (LLDs) and Petri Net-based (PN) approaches, do not currently possess the necessary mathematical support to guarantee the correct and effective implementation of computer control specifications in manufacturing systems.
The aim of this research is to develop a mathematically sound methodology for systematic incremental development of sequential control design problems, by enhancing the mathematics of the Knitting Synthesis Technique (KST) in PN theory. The design achieved via this methodology will have all the desired properties, which cannot be guaranteed by any of the existing approaches. In practice it will ensure that the LC desirable states are all reachable and the undesirable states (such as deadlock) will never be reached. This is an essential feature when complexity increases, as the viability of identifying mis-timing between loops, unexpected system states, etc. diminishes. Many PLCs are programmed via LLDs, a remnant of relay-based design, or developed in traditional high-level languages, such as C or Pascal. In any event, none of the existing development platforms are conducive to systematic design and testing of PLCs with large numbers of inputs and outputs and numerous control loops.
Many Programmable Logic Controller (PLC) applications require multiple concurrent control loops displaced in time-phase with the number of inputs and outputs in the order of tens or hundreds. An incorrect LC design may cause irreversible damage to quality and safety. The objective here is to minimise or eliminate such scenarios.
I will give a brief snapshot of the current status of the CZT tools plus a short demonstration. Then I will discuss plans for the future and a possible vision for how these tools might be used.