Scheduled Wiki Upgrade
Please note that the wiki upgrade will take place on the Wed 29th - Thurs 30th August 2018, during which time the wiki will be read-only. Click here for more information
We decided to take advantage of the concurrent visits of Makoto Takeyama and Yoshiki Kinoshita,
together with that of a few other local visitors, to run a sixth Bath-AIST workshop on 14 April 2010.
The details are as follows:
12.15 - 1.15 Lunch
1.15 - 2.15 Paul Levy (Birmingham): Nondeterminism, fixpoints and bisimulation
2.15 - 3.00 Yoshiki Kinoshita (AIST): Hoare in Agda
3.00 - 3.30 Break
3.30 - 4.15 Guy McCusker (Bath): Modelling local variables: possible worlds and object spaces
4.15 - 5.00 Temesghen Kahsai (Swansea): Property preserving development and testing for Csp-Casl
5.00 - 5.30 Makoto Takeyama (AIST): Assurance Cases in Agda
Nondeterminism, fixpoints and bisimulation (Paul Levy)
Denotational semantics of nondeterminism is an old subject, but many fundamental
problems remain, such as modelling bisimulation and fairness. This talk is a
survey of the state of the art in these problems.
On the one hand, we see counterexamples that pinpoint the difficulties. On the other,
I will indicate some lines of investigation that appear promising, using recent
technology such as game semantics and operational reasoning methods.
Hoare in Agda (Yoshiki Kinoshita)
I will talk about our shallow embedding of Hoare Logic in
Agda, which may also be regarded as soundness proof of Hoare Logic
written in Agda. This is joint work with Makoto Takeyama.
Modelling local variables: possible worlds and object spaces (Guy McCusker)
Local variables in imperative languages have been given denotational
semantics in at least two fundamentally different ways. One is by use
of functor categories, focusing on the idea of possible worlds.
The other might be termed event-based, exemplified by Reddy's
object spaces and models based on game semantics. O'Hearn and Reddy
have related the two approaches by giving functor category models
whose worlds are object spaces, then showing that their model is fully
abstract for Idealised Algol programs up to order two. But the
category of object spaces is not small, and so their functor category
is unlikely to be locally small. That means they cannot use the body
of results flowing from local smallness, such as cartesian closedness
of the functor category and its implications for their model. In this
talk we show how to refine their model by proving that the finite objects form a
small dense subcategory of a simplified object-spaces model, making
the induced functor category locally small, at the expense of being forced
to work in a Cpo-enriched setting.
Property preserving development and testing for Csp-Casl. (Temesghen Kahsai)
In this talk I will illustrate some development notions for the
specification language Csp-Casl. The latter is a specification language
that allows to specify data and processes in an integrated way.
These development notions are capable of capturing informal vertical
and horizontal software developments which we typically find in
industrial applications (e.g. electronic payment system).
On the other hand, such development notions allow us
to verify some interesting properties, e.g., deadlock or livelock freedom.
I will also present a theory for the evaluation of test cases with
respect to Csp-Casl specifications. With this approach, it is possible
to develop test cases for even the most abstract and basic
specifications, and to reuse them later on in more refined systems.
The presented theoretical results have been applied to the electronic
payment system EP2. Here, we have modeled the system in Csp-Casl,
verified properties using tool support and finally tested the system in
an hardware-in-the-loop testing framework.
Assurance Cases in Agda (Makoto Takeyama)
Assurance Cases are a key concept in communicating assurance of
computer systems' dependability among the stakeholders. They make
explicit arguments for claims on systems properties with supporting
evidences. They are large and complex documents that are hard to
construct and evaluate. We aim to introduce automation by formalising
cases as proofs in Agda. The adequacy of formalization process itself
becomes a problem for each case. We discuss writing styles for cases
in Agda that enables detailed review of the formalization by
From AIST (Japan):
Ana C. Calderon