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/ ***********************************************************