Skip to end of metadata
Go to start of metadata

We decided to take advantage of the concurrent visits of Nguyen Van Tang and Takashi Kitamura to run a fifth workshop at the University of Bath on the afternoon of 24 March 2010. The details are as follows:

Schedule

 11.15:      Grand Opening of the University of Bath Lovelace Laboratory
 12.15:      Lunch, in the Claverton Rooms
 13.15:      Talk: Takashi Kitamura
 14.30:      Talk: Andrew Lawrence and Monika Seisenberger
 15.00:      Talk: Karim Kanso and Anton Setzer
 15.30:      Break
 15.45:       Workshop/discussion based on Nguyen Van Tang's work and Agda
 17.30:       Talk: Nguyen Van Tang

From 1.15, the session will take place in 1W 2.7.

Titles and Abstracts

Takashi Kitamura

Title: A Logical Approach to Requirement Traceability and Domain Knowledge Elicitation

Andrew Lawrence and Monika Seisenberger

Title: Verifying Railway Interlockings using Scade

Abstract: This talk is concerned with the correctness of railway interlockings. The research
is carried out as a Master of Research in Logic and Computation project
in collaboration with the company Invensys Rail. The aim of the project is to
investigate whether the SCADE Suite from Esterel Technologies
is a suitable tool for carrying out the modelling and model checking
tasks involved in the verification of railway interlockings. By looking
at case studies conducted in previous MRes projects at Swansea
we will be able to make comparisons between the previous techniques
applied and the techniques used in the SCADE Suite.

Karim Kanso and Anton Setzer

Title: Model Checking from a Type Theoretic Perspective

Abstract: Theorem proving can be a complicated task; tools have been developed
to reduce the complexity, so that the user can focus on a simplified
core proof.

This project is concerned with the theorem prover and dependently typed
programming language, Agda. The problem of simplifying Agda proofs by
applying existing theorem provers is explored. An outline of a generic
connection is presented. Briefly this entails defining what it means
for a formula (i.e. propositional, LTL, CTL) to hold w.r.t. a model,
defining a decision procedure and proving its correctness in Agda.

As a case study of the above mechanism, the model checking theory is
presented.

Workshop/discussion:

Title: A Hybrid Approach to Verify A Train Fare Calculation System Using Testing

Abstract: In this talk, I will present our work on verification of a large-scale software system (Japanese train fare calculation system) in practice. This is a collaborative research project between AIST/CVS and a company. I will briefly present our main formal verification techniques to verify the system, such as VDM (Vienna Development Method) specification languages + Agda (a functional programming languages and theorem prover).

Nguyen Van Tang

Title: On-the-fly Universality and Inclusion Checking for Visibly Pushdown Automata

Abstract: Visibly pushdown automata (VPA), introduced by Alur and Madhusuan in
2004, is a subclass of pushdown automata whose stack behavior is
completely determined by the input symbol according to a fixed
partition of the input alphabet. Since its introduce, VPAs have been
shown to be useful in various context, e.g., as specification
formalism for verification and as automaton model for processing XML
streams. Due to high complexity, however, implementation of formal
verification based on VPA framework is a challenge. In this paper we
consider the problem of implementing VPA-based model checking
algorithms. For doing so, we first present an improvement on upper
bound for determinization of VPA. Next, we propose simple on-the-fly
and antichain-based algorithms to check universality and inclusion problems of this
automata class. Then, we implement the proposed algorithms in a
prototype tool. Finally, we conduct experiments on randomly
generated VPAs. The experimental results show that the proposed
algorithms are considerably faster than the standard ones.

Participants:

from Bath:

Ana Calderon
Martin Churchill
Jim Laird
Guy McCusker
Julian Padget
John Power
Alexei Strelnikov

from AIST:

Takashi Kitamura
Nguyen Van Tang

from Swansea:

Karim Kanso
Andrew Lawrence
Monika Seisenberger
Anton Setzer

  • No labels