TTSS'07 - List of Accepted Papers

TITLE

AUTHOR

Generic tools via general refinement

Steve Reeves and David Streader

Abstract

Shape Analysis by Refining on Abstract Evaluation Path

Xiaodong Ma, Ji Wang and Wei Dong

Abstract

On Verification of Linear Occurrence Properties of Real-Time Systems

Chang Il Choe and Van Hung Dang

Abstract

Engineering of An Assertion-based PSL-Verilog Dynamic Verifier by Alternating Automata

Naiyong Jin, Chengjie Shen and Jun Chen

Abstract

Prototyping System Requirements Model

Xiaoshan Li and Jifeng He

Abstract

Barbed Model-Driven Software Development: A case study

Carlo Montangero and Laura Semini

Abstract

An exercise on transition systems

Paula R. Ribeiro, Luis Barbosa and Shuling Wang

Abstract

Parametric Analysis of an Improved Fault Tolerant System

Miaomiao Zhang

Abstract

Integrating refinement into software development tools

Lu Yang

Abstract

Pre-Galois Connection on Coalgebras for Generic Component Refinement

Meng Sun

Abstract

A Rigorous Model of Service Component Architecture

Zuohua Ding and Jing Liu

Abstract

The Verification of rCOS Using SPIN

Xiao Yu and Zheng Wang

Abstract

Steve Reeves and David Streader. Generic tools via general refinement

Abstract: Tools have become essential in the formal model-driven development of software but are very time consuming to build and often restricted to a particular semantic interpretation of a particular syntax. This is regrettable since there is large amount in common between tools, even if they do implement different syntaxes and different semantics.

We propose splitting tools into front- and back-ends where an operational semantics acts as the link between the two. We will not have much to say about the front-end and the link in this paper since it is theoretically straightforward. Instead, we concentrate on the second part and provide a well-motivated, general, mathematical framework to form the underlying theory that gives great flexibility to the back-end of a tool which is concerned with developing software via stepwise refinement.

From a general model of refinement between two entities, where the refinement is parameterised on contexts and observations, we build logical theories which have refinement as implication. Further, we consider what can be expected of a guarantee concerning the behaviour of an implementation relative to a specification. Then by fixing the contexts and observations in suitable ways, and so getting particular, special models of refinement, we give a formal interpretation of a guarantee. To this we add theory morphisms between special models, where a  theory morphism can change the contexts and observations we can make in controlled and useful ways, mainly by preserving a refinement relation between entities even as we change them.

We show how the generality brought about by the parameterisation allows an example from the literature, which seems formally not to be a refinement, to be captured as one, thus according with our intuitions about the example.

In this way we show the flexibility of our theory for a refinement tool back-end. From this it follows that the effort put into building a tool based on our theory will be well-spent---a single tool should be parameterised (just as our theory is) to deal with the many different notions of refinement found in the literature. Thus we make a contribution to the problem of ensuring correctness and dependability of software using formal methods and tools of modelling, design, verification and validation.

Xiaodong Ma, Ji Wang and Wei Dong. Shape Analysis by Refining on Abstract Evaluation Path

Abstract: This paper presents a novel method for shape analysis, which can deal with complex expressions in C language. It supports taking addresses of fields and stack variables. The concept of abstract evaluation path (AEP) is proposed, which is generated from the expression in the language. AEP is used to refine the
abstract shape graph (ASG) to get a set of more precise ASGs, on which the semantics of the statement can be defined easily. The results can be used to determine shape invariants and detect memory leak conservatively. A prototype has been implemented and the results of the experiment is shown.

Chang Il Choe and Van Hung Dang. On Verification of Linear Occurrence Properties of Real-Time Systems

Abstract: Duration Calculus of Weakly Monotonic Time (WDC) is an extension of DC to allow description of discrete processes where several steps of computation can occur at the same time point. In this paper, we introduce Linear Occurrence Invariants (LOI) using WDC and give an algorithm to check real-time automata for LOI by solving integer programming problems. LOI can be used effectively to specify system requirements in some cases including when the
system is considered under the true synchrony assumption. We also extend WDC probabilistically to express dependability requirements of real-time systems and develop a technique to check deterministic probabilistic real-time automata for a class of probabilistic WDC formulas.

Naiyong Jin, Chengjie Shen and Jun Chen. Engineering of An Assertion-based PSL-Verilog Dynamic Verifier by Alternating Automata

Abstract: Alternating Finite Automata (AFA) has linear space complexity in representing Linear-Time Temporal Logics. However, It is difficult to manipulate AFA in the run-time. In this paper, we focus on implementation methods to make alternating automata from static representation to run-time verification engines. 1) We have Directed Acyclic Graphs (DAG) represent all possible runs of a Local-variable-enhanced AFA (LAFA). The acceptance of universal choices is conditioned on successful synchronization of universal branches. 2)We encode states and local variables by symbolic approaches. The encoding enables multiple assignments to states and local variables in a configuration. Different values of a state or variable stand for different execution results of a LAFA. By those methods, we are able to maintain the linear complexity of verification in both space and time.

Xiaoshan Li and Jifeng He. Prototyping System Requirements Model

Abstract: In this paper, we present a tool for automatic prototype generation and analysis(AutoPA2.0) that implements the transformations from UML system requirements models to executable prototypes with the function of checking multiplicity constrains. A UML system requirements model consists of a use-case model and a conceptual class model. Each use case is either described as a pair of pre and post conditions in the context of the conceptual model or represented as an activity diagram drawn by the user. AutoPA2.0 can transform the descriptions of use cases in activity diagrams or pre and post conditions into an executable prototype in Java. The prototype of a requirements model can be used to validate dynamically the requirements by checking the pre and post conditions of the use case operations, and system invariants. It helps to improve the understanding between customers and designers. A simple library system is used to illustrate the feasibility of tool as well as its development.

Carlo Montangero and Laura Semini. Barbed Model-Driven Software Development: A case study

Abstract: When thinking to Model Driven Engineering, the picture appearing to our eyes is that of a sequence of models, from the  most abstract one to the most concrete one. However, model transformations can deviate, as barbs, from the development sequence. This is done, for instance, to apply verification techniques and tools to the models at the intermediate stages. In our opinion, this subject deserves more attention and a better understanding than the one received till now.

To focus on barbs, and assess their influence on the main development process, we experiment on a case study where we check the security properties held by the UML model of a distributed system.

Paula R. Ribeiro, Luis Barbosa and Shuling Wang. An exercise on transition systems

Abstract: Labelled transition systems admit different but equivalent characterizations either as relational structures or coalgebras for the powerset functor, each of them with their own merits. Notions of simulation and bisimulation, for example, are expressed in the pointfree relational calculus in a very concise and precise way. On the other hand, the coalgebraic perspective regards processes as inhabitants of a final universe and allows for an intuitive definition of the semantics of process combinators. This paper is an exercise on such a dual characterisation. In particular, it discusses how a notion of weak bisimilarity can be lifted from the relational to the coalgebraic level, to become an effective reasoning tool on coinductively defined process algebras.

Miaomiao Zhang. Parametric Analysis of an Improved Fault Tolerant System

Abstract: We report our preliminary study on an improved triple modular computer system from the aerospace field, which is designed to compute the course of action that other subsystems take and output the result to other subsystems. Based on the formal model of the system, we derive constraints on the values of the parameters that occur in our model, and manually prove that ``When a CPU is in the startup phase, it should not restart again due to its watchdog timer overflow or a restart signal sent from the arbitrator".

Lu Yang. Integrating refinement into software development tools

Abstract: Most of the existing work on formally automated software engineering is about verification and validation, such as model checking, static checking, runtime monitoring and testing. There is little progress in automatic tool support to formal design by refinement transformations. In this paper, we bring this matter to the attention of the research community and discuss a component-based model transformational approach for integrating refinement into software development tools. Models, their consistency and correctness, in an object-oriented and component-based development process are defined in rCOS, that is a refinement calculus recently developed at UNU-IIST. Correctness preserving transformations between models are formalized and proved as refinement rules in rCOS. In this paper, we will discuss on how these transformations can be implemented in the relations language of Query/View/Transformation (QVT) standardized by OMG.

Meng Sun. Pre-Galois Connection on Coalgebras for Generic Component Refinement

Abstract: The technique of Galois connections has been applied successfully in many areas of computer science. By employing coalgebras as models for software components, we claim that different forms of behavior model and types of state transitions for components are instances of a single form of coalgebra in a Kleisli category. Based on the Kleisli category, the results on forward/backward morphisms and refinement of components in Set are still satisfied in this more generic framework. We propose a notion of pre-Galois connection in the context of coalgebras for refinement of state-based software components which takes into consideration not only the refinement ordering but also the dynamics of the components, and we study its properties in the Kleisli category. This notion is a powerful tool for relating a component to its refinement and for relating a component to its abstraction. Thus it provides a basis for reasoning about state-based software designs and reverse engineering.

Zuohua Ding and Jing Liu. A Rigorous Model of Service Component Architecture

Abstract: Service Component Architecture (SCA) provides a platformindependent component model for service-oriented development. The service component with different commutation mechanisms and implementing languages can be modeled in SCA. However, it lacks of a formal foundation for specification and verification SCA-based system. This paper presents a formal service component signature model with respect to the specification of the SCA assembly model. Inspired by the idea of independence in SCA, a language-independent dynamic behaviour model is proposed for specifying the interface behaviour of the service component by port activities. Based on the dynamic behaviour model, the compatibility relation between components is discussed as well as refinement. A set of transition rules are given to map BPEL to dynamic behaviour expressions and then to Petri nets, thus the service component based system can be verified with existing tools. A case study is demonstrated to illustrate how to use our approach to constructing a web application in a rigorous way.

Xiao Yu and Zheng Wang. The Verification of rCOS Using SPIN

Abstract: rCOS is a relational object-based language with precise observation-oriented semantics. It can capture the key features of object model including subtypes, visibility, inheritance, polymorphism and so on. To analyze the model specified by rCOS, we propose a verification approach to check whether the constrain such as the assertion, invariant of class and method contracts hold. Firstly, the Promela code is generated from rCOS specification according to the mapping rules. Secondly, we call the SPIN engine to verify the generated PROMELA codes. Thirdly, if an error is reported by SPIN, a trace algorithm is applied to locate the error in the original rCOS model. Furthermore, to enhance the ability of rCOS to model concurrency, we extend the original rCOS with parallel structure and develop synchronization mechanism. A case study is presented to show how our approach works.