Dimitra Giannakopoulou visited SRI international on Monday 3 May 1999. The objective was to exchange experience in the area of capturing system requirements in software architectures, and analysing such architectures with respect to desirable properties. Both the Imperial College and the SRI group have developed their respective architecture description languages (ADLs), Darwin and SADL. In addition, they work on developing methodologies to formally reason about properties of architectures. The approaches taken are different: the group at Imperial combines structural descriptions with behavioural ones, and applies highly automated analysis techniques based on model checking. The group at SRI provides the facility to refine architectures with steps that preserve specific properties of interest, and uses theorem proving to reason about correctness requirements.

The following activities were held during the visit:

Discussion with Victoria Stavridou, head of the dependable software architectures group, about the aims of their research work, and the current status of their methods and tools. The group is oriented towards developing techniques to support refinements of software architectures that preserve various kinds of properties such as security and dependability. Work has been performed in the past in proving that architecture refinement preserves some architectural style. Experience has also been obtained from case studies such as that of that of the X/Open standard for distributed transaction processing (DTP). The group has worked on adding multi-level security aspects to the standard, and an implementation was demonstrated by Fred Gilham. The project was based on a Rapide description of the architecture in the X/Open standard. The Rapide description was translated to SADL, and a number of refinements were performed towards the implementation (each refinement step was performed and proven manually). The goal is to be able to provide automated support in the process of refining software architectures.

Discussion with Bruno Dutertre and Hassen Saidi about attaching behaviour to software architectures and abstraction methods. Dimitra Giannakopoulou and Hassen Saidi also discussed their respective experiences with the (industrial) case study of the Phillips Bounded Retransmission Protocol, which is a good example of applying abstraction techniques.

Discussion with Robert Riemenschneider related to SADL, patterns for refinement of software architectures and the current status of tool support for their methods. A previous tool developed by the group and used in an industrial setting was discussed. The group is also working on the issue of automatically transforming architectural proofs at each refinement step. This would facilitate the task of the user since either the proof can be transformed, or some parts remain to be added by the user. In both cases, the effort required is less than starting a proof from scratch.

Dimitra Giannakopoulou gave a seminar on "Behaviour analysis based on software architecture", and presented the Tracta approach. Specifically, she described the way in which software architecture descriptions in Darwin are used in Tracta to drive both modelling and analysis of a computing system. She also demonstrated the LTSA model-checking tool that supports Tracta.

Discussion with John Rushby and Natarajan Shankar on model checking and theorem proving. The discussion followed the seminar, which started a number of interesting issues: potential improvements to the LTSA model-checking tool developed at Imperial, comparison with existing tools such as Caesar Aldebaran, and finally SAL, a system that is currently under development by the formal methods group. The latter is intended to link existing verification tools by translating specifications in any of a number of languages to some intermediate form, which can then be used as input for the tools that will be supported.

The possibility was discussed for a longer visit of Dimitra Giannakopoulou to SRI.

Last update: 25 May 1999