BCS-FACS Christmas Meeting
Formal Methods and Testing
19 December 2005
BCS London Offices
First Floor
The Davidson Building
5 Southampton Street
London WC2E 7HA
http://www.bcs-facs.org/events/xmas2005.html
With the growing significance of computer systems within industry and
wider society, techniques that assist in the production of reliable
software are becoming increasingly important. The complexity of many
computer systems requires the application of a battery of such techniques.
Two of the most promising approaches are formal methods and software
testing.
This is the topic investigated within the FORTEST network and the focus of
this meeting
This workshop is organised by Rob Hierons (Programme Chair) and
Paul Boca (Local Organizer). The event will consist of six talks:
Dines Bjorner, Technical University of Denmark,
Two Models of Communication Transaction Processes -
or why our colleagues are letting us down!
Abstract
There exists a proceedings paper proposing a rather nice concept,
Communication Transaction Processes, or CTP, in which Petri Nets and
"blended"
with Message Sequence Charts. That 2003 ACSD'03 paper (A. Roychoudhury and
P.S. Thiagarajan)
uses what seems classical means of presenting the syntax and semantics of
CTPs.
With a PhD student of Thiago's (Mr Yang Shaofa) I worked out an alternative
Raise/RSL model.
In doing so Mr. Yang Shaofa uncovered a number of inconsistencies and
incompleteness of
the ACSD'03/CTP paper. Their communication to the original authors basically
went unanswered.
In the talk I will hint at the two models and then I will lament on the sad
fact, apparently,
that our colleagues, in casu AR+PST, seem unaware that formal specifications
in the style of
for example B, VDM, RSL or Z appear (a claim) to be far better at doing a
proper job.
The talk suggests that lack of progress in transferring formal methods to
industry may also
be due to our candidates not taking FMs serious as long as their professors
don't.
Mark Josephs, London South Bank University,
Controllable Delay-Insensitive Processes
Abstract
Delay-insensitive processes interact by engaging in a sequence of inputs and
outputs.
The initial behaviour of a process is characterized by whether or not it is
divergent,
what it might output, and whether or not it can refuse to output. This leads
in a natural way
to a refinement ordering whereby one process can be substituted for a less
deterministic one,
as in Hoare's CSP. A recent insight is that a process is controllable if it
can continually
interact with some other process (a friend) without causing interference or
deadlock.
The reflection of a controllable process is then its most non-deterministic
friend.
By restricting ourselves to controllable processes, we are able to obtain
the links between refinement,
reflection and factorization, previously demonstrated by Dill and Verhoeff.
Mark Harman, Kings' College London,
Testability Transformations
Abstract
This talk discusses ways in which we can improve software testability using
transformations.
The transformations to be used are novel because they need not preserve
traditional notion
of equivalence. In the conventional sense they are not therefore meaning
preserving transformations.
However, they are adequate test set preserving. The approach is also novel
because the transformations
are not an end but a means to an end; once the test data is generated, the
transformed program can be
discarded.
Paul Krause, University of Surrey,
Modelling Components in an Uncertain World
(work by Sotiris Moschoyiannis, Mike Shields and Paul Krause to be presented
by Paul Krause)
Abstract
The move to a component-based way of working in software engineering has
much potential in terms
of reducing cost and time to market. However, experience in developing
complex applications shows
that significant effort is still needed to solve component integration
issues in domains that exhibit
high levels of concurrency. This talk will present a formal framework for
managing the dependencies
between components, in terms of their interactions in a concurrent setting.
In our approach, composites and single components are represented by a
component signature, which
identifies a component, and a vector language, which describes the behaviour
of a component.
This language-based representation of component behaviour makes it possible
to capture concurrency at
both the individual component level and the composition level. The
interpretation of concurrency is
that of a non-interleaving model, with the notion of causal independence
lifted to vectors.
We describe how component languages are obtained from the informal
scenario-based specifications that
are typical in an industrial context.
This formal framework for components has been related to more conventional
approaches to software design,
as exemplified by strong connections to UML. It can aid designers in
determining the complete set of
intended behaviours before generating state models of the scenario-based
specifications. These models
can then be used to better inform developers, and generate extensive test
sets for the final product.
Paul Baker, Motorola Research,
Model Based Development at Motorola
TBA
The programme and abstracts of the talks can be found on the workshop
website. If you would like to attend the workshop, please download
a registration form from
http://www.bcs-facs.org/events/xmas2005/registration.html
The cost of attending is £40 (incl. VAT) for paid-up BCS-FACS members
and £60 (incl. VAT) for non-FACS members. Registration fees include
a year's free subscription to the Formal Aspects of Computing Science
Specialist Group.
Refreshments, a buffet lunch and wine reception (with mince pies!) are
included in the price.
As well as attending some interesting talks and having a festive drink
with colleagues, you'll be able to do some last minute Christmas shopping
in the West End of London. Tempted? Then register for the event now!
Sponsor: The British Computer Society
***********************************************************
Professor Robert M. Hierons
School of Information Systems, Computing, and Mathematics,
Brunel University,
Uxbridge, Middlesex,
UB8 3PH United Kingdom
phone +44 (0) 1895 266002
fax +44 (0) 1895 251 686
email [log in to unmask]
homepage http//people.brunel.ac.uk/~csstrmh/
***********************************************************
|
