Dependable Computer-Based Systems

Program Leaders: Geoff Dromey, Ian Hayes, Peter Lindsay

The rapid pace of advances in Information and Communications Technology (ICT) has led to technological systems of ever increasing complexity and sophistication. Many of these systems – in areas such as transport, health and finance – need to be safe, reliable and generally dependable. There is a constant need for new methods and tools to enable engineers to ensure that such systems meet society’s demands for dependability. This program was concerned with the development of modelling and analysis tools to ensure that dependability is designed into complex computer-based systems.

 

Projects:

Building dependability into complex computer-based systems

Project Leaders: Geoff Dromey, Ian Hayes, Peter Lindsay
Researchers: Maria Aneiros, David Carrington, Rob Colvin, Lars Grunske, Diana Kirk, Toby Myers, Danny Powell, John Seagrott, Cameron Smith, Lian Wen, Kirsten Winter, Nisansala Yatapanage, Saad Zafar, Xuelin Zheng

Large-scale, complex, software-intensive systems can be made more dependable by constructing comprehensive  formal graphical models of their behaviour. These models need to clearly show how individual functional requirements interact with one another. They also need to show how safety, security, reliability and other types of dependability requirements are manifested as supporting behaviour that coherently integrates with the functional requirements. Ultimately all the functional and dependability requirements must integrate to preserve the overall behavioural integrity of a system. Adopting the underlying constructive development strategy of building a system out of its requirements, offers a promising approach for dealing with large-scale systems, building in dependability and assuring dependability while at the same time coping with change, requirements defects and the complexity of such systems. The Behavior Tree notation and supporting design and analysis methodology enables the investigation of constructive development and the creation of integrated views of requirements. Using this approach the project explored practical ways of engineering in and systematically assuring the dependability of large-scale and complex systems. (Included 2005/06 summer project)

The initial focus of this project was on identifying functional and dependability requirements at both system and component levels. The project aimed at better, integrated approaches for modelling requirements, developing architecture and design that meets those requirements, and providing their assurance. The approaches need to cope with the scale, change and unpredictability associated with large systems. The project investigated the use of the Behavior Tree Notation for modelling large sets of functional requirements that are typical for complex engineered systems. The goal was improved requirements analysis and traceability, which are commonly regarded as key areas for improving system dependability. To provide an unambiguous semantics of the Behavior Tree Notation we proposed formalisations using CSP, and a strongest postcondition semantics. The CSP formalisation of a Behavior Tree reflects its component structure modelling interacting processes, whereas the strongest postcondition semantics allows reasoning about properties of system states. Thus, the two formalisations focus on different issues and provide different possibilities for support with analysis tools. Both semantics provide the basis for tool support to validate that the system meets its intended requirements. As a modelling notation for requirements and system design, Behavior Trees are targeting the same issues as the UML notation. Our aim was to compare the facilities of both notations.

A set of tools was developed to support the approach. These included tools to help the user specify the system (editors) as well as tools to check properties of the integrated set of requirements. Problem independent checks can be performed directly on the Behavior Tree using simple tree walking algorithms to extract information that can be checked for consistency and completeness. Behavior Trees can be translated to existing formalisms in order to make use of tools for analysing those formalisms. We investigated translation to CSP to use the FDR analysis tool. As well as checking properties of the system, we can also check if a refinement relation holds between the specification and implementation of a system. In addition, we investigated translation of Behavior Trees to the SAL notation to use its model checking tools. We investigated the explicit modelling of both the normal behaviour of components as well as likely faulty behaviour, in order to perform analysis of the system response to component faults.

Substantial progress was made on tool development and theory in 2004. Precondition analysis and safety checks were incorporated into the Behavior Tree (BT) editor. The editor was also improved to support a more information rich BT structure, which allowed generation of CSP models, and a translator from Behavior Trees to CSP was implemented. This enabled the use of the FDR model checking tool to analyse the translated model for a set of functional requirements. With CSP we can check if a refinement relation holds between the specification and implementation of a system. Behavior Tree notation was extended to support mixed branches involving concurrent events on different components.

A component testing software package was developed which creates component interface diagrams from Behavior Trees and uses them to test component implementations written in either Java or .NET languages. We explored the use of BTs for Failure Modes and Effects Analysis, by systematically replacing functional requirements by faulty variants; a translation to Action Systems was then developed, so that a model checker could be used to identify which faults could lead to hazards. The Failure Analysis Software package, BTFail, was completed and merged it into the Behavior Tree Editor. Behavior Trees have been used to model an autonomous shuttle system. In addition, they have been used to model Branching Regulatory Network in peas; this work was done in collaboration with Dr J. Hanan and Dr. C. Beveridge from Centre for Plant Architecture Informatics.

In 2006, we have focused on scaling-up the Behavior-Tree methodology to handle industry-scale systems with very large numbers of natural language requirements. As part of this work, we have conducted successful trials in using the method with a number of industrial partners. We have also made an important advance that allows us to build a security policy into a design and then verify that the design satisfies the policy. With the increased usage of wireless LANs, security is a significant issue. The latest WLAN security protocol, the IEEE 802.11i assures rigorous security for wireless networks with its protocol for authentication, authorisation and key distribution. We have developed a Behavior Tree model for the IEEE 802.11i Robust Security Mechanism and used the SAL model checker to formally verify the protocol.

  • Dromey, R.G., 'Formalizing the transition from requirements to design', Mathematical Frameworks for Component Software - Models for Analysis and Synthesis, World Scientific Series on Component-Based Development, World Scientific Publishers, 2006, 156-187.
  • Dromey, R.G., ‘Genetic design: Amplifying our ability to deal with requirements complexity’, Lecture Notes in Computer Science, vol. 3466, 2005, 95–108.
  • Dromey, R.G., 'Keynote Address - Guiding principles for engineering quality software', 2nd Malaysian Software Engineering Conference (MySEC’06), 2006.
  • Dromey, R.G., 'Scaleable formalization of imperfect knowledge', 1st International Workshop - Asian Working Conference on Verified Software (AWCVS’06), Oct 2006, 21-33.
  • Dromey, R.G., "Using Behaviour Trees to model the autonomous shuttle system", 3rd International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools (SCESM04) ICSE Workshop W5S, Edinburgh, 2004.Dromey, R.G., Powell, D., ‘Early requirements defects detection’, TickIT Journal, no. 4Q05, 2005, 3–13.
  • Grunske, L., Geiger, L., Zündorf, A., VanEetvelde, N., VanGorp, P., Varró, D., ‘Using graph transformation for practical model driven software engineering’, Model-Driven Software Development - Volume II of Research and Practice in Software Engineering, Springer Verlag, 2005, 91–119.
  • Grunske, L., Kaiser, B., ‘An automated dependability analysis method for COTS-Based systems’, ICCBSS 2005, February 2005; Lecture Notes in Computer Science, vol. 3412, 178–90
  • Grunske, L., Lindsay, P., Yatapanage, N., Winter, K., ‘An automated failure mode and effect analysis based on high-level design specification with Behavior Trees’, 5th International Conference on Integrated Formal Methods (IFM 2005), 2005; Lecture Notes in Computer Science, vol. 3771, 129–149.
  • Fitzgerald, J., Hayes, I.J., Tarlecki, A., FM 2005: Formal Methods - Proceedings 13th International Symposium of Formal Methods Europe, Newcastle, UK, July 2005, Lecture Notes in Computer Science, vol. 3582, Springer Verlag, July 2005.
  • Hamoy, C., Hemer, D., Lindsay, P., "HazLog: tool support for hazard management", Proc 9th Australian Workshop on Safety Critical Systems and Software, 2004.
  • Hemer, D., Lindsay, P., ‘Template-based construction of verified software’, IEE Proc Software, vol. 152, no. 1, February 2005, 2–14.
  • Lermer, K., Fidge, C.J., Hayes, I.J., ‘A Theory for Execution Time Derivation in Real-time Programs’, Theoretical Computer Science, vol. 346, no. 1, November 2005, 3–27.
  • Smith, C., Winter, K., Hayes, I.J., Dromey, R.G., Lindsay, P., Carrington, D., "An environment for building a system out of its requirements", Proceedings of the 19th IEEE International Conference on Automated Software Engineering, 2004, 398-399.
  • Winter, K., "Formalising behaviour trees with CSP", Integrated Formal Methods, April 2004; LNCS, Vol. 2999, 148-167
  • Zafar, S., Dromey, R.G., ‘Integrating safety and security requirements into design of an embedded system’, Proceedings of the Asia-Pacific Software Engineering Conference, 2005, 629–636.
  • Zafar, S., Dromey, R.G., ‘Managing complexity in modelling embedded systems’, Proceedings of Systems Engineering/Test and Evaluation Conference (SETE 05), 2005.
  • Zafar, S., Winter, K., Colvin, R., Dromey, R.G., 'Verification of an integrated role-based access control model', 1st International Workshop - Asian Working Conference on Verified Software (AWCVS’06), Oct 2006, 230-240.

AutoGuard: An interactive development environment for relative debugging of programs

Project Leader: David Abramson
Researchers: Clement Chu, Donny Kurniawan, Aaron Searle

Software systems are among the most complex systems developed by humans. This project developed methods and tools to help software engineers debug their programs. Relative debugging involves comparing one program with another, to determine where they will diverge when being executed. In particular, the contents of key data structures in a development version are compared with the contents of the corresponding data structures in an existing version as the two programs execute. If the values of two corresponding data structures differ at points where they shouldn’t, an error may exist and the developer is notified. The aim of this project was to explore three significant research opportunities in relative debugging, a technique David Abramson had pioneered in 1993. First, we wanted to enhance our command line version of our relative debugger, called Guard, so it could be embedded into interactive development environments (IDEs). Second, we wanted to build an interactive browser that could present the data-flow of a program graphically, and in particular show the define and use points for variables. This would then allow a user to create the assertions required in relative debugging more easily. Third, we suggested that it would be possible to completely automate the process of assertion generation and program execution under certain circumstances. Under these conditions, it would be possible to present two programs to the system, and for the divergence between the execution of the two programs then to be deduced automatically.

During 2004, we have produced a relative debugger embedded in three difference IDE’s, namely the Microsoft Visual Studio .NET environment, IBM’s Eclipse and SUN’s One Studio. We constructed a dataflow browser called DUCT, that allows a user to traverse the USEDEFINE chains of any given variable. This function is performed on demand, and it builds a control flow graph of the program using static analysis techniques. This graph can then be used to locate the most likely definitions of variables given the static analysis. We have developed a number of new techniques that demonstrate significant progress towards our third aim. To do this DUCT has been modified so that it produces the entire DEFINE-USE tree for all variables, and these are used to generate assertions for all data structures. This provides the necessary infrastructure to automatically compare programs that are written in different languages. These assertions are then loaded into Guard using a special API that allows an external program to control the debugger. The system has been tested on a number of small programs and the results show that it is possible to automatically generate assertions under certain circumstances.

In 2005, PhD student Aaron Searle continued to develop techniques for automatically comparing the execution of two executing programs. Using sophisticated analysis techniques he was able to generate assertions automatically and these are used by the debugger to test the internal state of the programs, which enables divergence between the execution of the two programs to be deduced automatically. He is currently completing his PhD thesis on this topic.

Also in 2005, we added parallel support for our initial IBM Eclipse based relative debugger, EclipseGuard. This now allows a user to compare the state of two parallel programs whilst controlling the work from within a powerful integrated development environment. Finally, we have started a new thread to extend the work to support development and debugging of software systems for the Grid. This latter effort is being undertaken by PhD student Donny Kurniawan and will define a WSRF compliant architecture for debugging software. The project also underpins a collaboration with the Los Alamos National Laboratories (LANL) concerning the development of a parallel debugger plug in for Eclipse, and together with colleagues at LANL, we have made progress towards this goal.

During 2006, the outcome of this research is the discovery of techniques that empower Relative Debugging users to become more productive and allow the Relative Debugging paradigm to be significantly enhanced. Specifically, the research has resulted in the following three contributions: 1. Formalisation of the Relative Debugging Methodology; 2. Data Flow Browsing for Relative Debugging; and 3. Automatic Relative Debugging. These contributions have enhanced the Relative Debugging paradigm and allow errors to be localised with little or no human interaction. Minimising the user’s involvement reduces the cost of debugging programs that have undergone software evolution. Automating the Relative Debugging paradigm reduces the need for users to have a detailed knowledge of the programs under consideration, thereby improving productivity and has a significant impact on current debugging practices.

Model translation with MDA and XMI

Project Leaders: Kirsten Winter, Lars Grunske
Researcher: Bangjun Chen

The Behavior Trees notation enables system and software requirements to be modelled graphically. This project aimed to build a rule-based translator that transforms Behavior Trees into UML and/or CSP. All three notations (Behavior Trees, UML and CSP) can be represented in XMI.

In 2004 an XMI meta-model was developed for Behavior Trees and an export function was implemented for the BTE tool. (Summer Project 2004/05).

Change management: Formalising the impact of requirements change on design

Project Leader: Geoff Dromey
Researchers: Toby Myers, Peter Fritzson, Lian Wen

This project used Behavior Trees to model requirements change. One aspect was the investigation of a formal process to map the changes from the functional requirements into the software design, which includes the component architecture, the component behaviours and the component interfaces. The other aspect was the investigation of the impact of change of functional requirements on the component architecture, and how this impact may be reduced or prevented, thereby making the software system more stable and easier to maintain. 

 In 2004, the mapping from requirements change to design change were formalised. This allows changes in requirements to be automatically reflected in the architecture, the component interfaces, and the component designs.

In 2005, there have been two significant achievements with this project – one theoretical and one practical. The theoretical result shows how it is possible, by applying an appropriate sequence of transformations, to change from one architecture to some target architecture without changing the behaviour or impacting the set of functional requirements that a system satisfies. This very general and significant result has been written up in an international conference paper on architecture normalisation. The other significant development has been the completion of a tool to support the change component-based designs. This tool implements the theoretical results obtained and published in 2004.

In 2006, the theoretical work previously carried out on changing the architecture of a system has been extended to include a new target architecture without changing the behaviour or the set of functional requirements the system satisfies. The results of this work have been published in a journal article. We have also extended the theoretical work undertaken on systematically mapping requirements changes to traceable changes in design work products. This has involved versioning the different sets of changes, resulting in a model where the changes in each version can be traced and recovered. The results have been written up and are to be submitted to a journal. Lian Wen has also submitted his PhD thesis on the work completed in this area.

In 2007, we submitted a paper on evolutionary change of systems to the journal ACM Transactions of Software Engineering.

  • Myers, T., Dromey, R.G., “From requirements to embedded software—Formalising the key steps”, Australian Software Engineering Conference (ASWEC), 2009.
  • Myers, T., Fritzson, P., Dromey, R.G., “Seamlessly integrating software and hardware modelling for large-scale systems”, Proceedings of the 2nd International Workshop on Equation-Based Object-Oriented Languages and Tools, 2008, 5–15.
  • Wen, L., Dromey, R.G., 'Architecture normalization for component-based systems', Electronic Notes in Theoretical Computer Science, Vol. 160, 2006, 335-348.
  • Wen, L., Dromey, R.G., "From requirements change to design change: A formal path", SEFM 2004, IEEE International Conference on Software Engineering and Formal Methods, 2004, 104-113.Wen, L., Kirk, D., Dromey, R.G., “A tool to visualize behavior and design evolution”, International Workshop on Principles of Software Evolution (IWPSE2007), 114-115, 2007.

Collaborative software engineering based on Behavior Trees

Project Leader: Chengzheng Sun
Researchers: Geoff Dromey, David Chen, Kevin Lin

A Real-time Collaborative Genetic Software Engineering system (CoGSE) allows a group of users to view and edit the same Behavior-Tree representation at the same time from different sites. To develop CoGSE, we investigated constraint maintenance in collaborative systems. Constraint maintenance is an important issue in single-user CAD and CASE tools. In collaborative systems, constraint maintenance becomes even more complicated due to the generation and execution of various combinations of concurrent and dependent operations. In CoGSE, constraint maintenance is required to maintain Behavior-Tree structure and to resolve conflicts. Tasks include multi-user editing of Behavior Trees, visualization methods and collaborative computing methods.

In 2004, a strategy was developed for maintaining constraints. It involves duplicating components to maintain tree-structure representation in a collaborative setting. A prototype collaborative Behavior Tree editor has been implemented.

In 2005, we investigated the new features of collaborative systems with constraints, such as the difference between conflicts and constraint violations, the interferences among constraints in collaborative systems, etc. In particular, we have proposed a masking strategy that is able to maintain both constraints and system consistency in the face of concurrent operations. The strategy is independent of the execution orders of concurrent operations and able to retain the effects of all operations in resolving constraint violation. The proposed strategy can be adopted to enforce tree structure constraint in CoGSE, and maintain constraints in many kinds of collaborative systems as well. Moreover, we have proposed an approach to reconstruct computation flows to maintain dataflow constraints when concurrent user operations modify the constrained variables in collaborative systems.

In 2006, research has concentrated on the issues of constraint maintenance in collaborative environments. In particular, how to maintain multi-way dataflow constraints, which are widely applied in various interactive single-user systems, in collaborative systems. A constraint maintenance algorithm has been developed which produces a constraint propagation effect that is consistent with the underlying syntax level execution effect. Furthermore, constraint propagations are performed only when no user operation is waiting for execution which, in turn, improves system responsiveness. This method has been presented in a conference paper. The other major development this year has been the incorporation of the collaborative editing facility for Behavior Trees into the new Integrare Collaborative Tool Environment.

In 2007, an editing tool for Behavior Trees was designed and a collaborative facility was implemented. The resulting tool was used for developing many of the case studies used by other sub-projects in this research stream.

  • Lin, K., Chen, D., Dromey, R.G., Sun, C., “Maintaining constraints expressed as formulas in collaborative systems”, 3rd International Conference on Collaborative Computing: Networking, Applications and Worksharing, November 2007.
  • Lin, K., Chen, D., Dromey, R.G., Sun, C., ‘Maintaining multi-way dataflow constraints in collaborative systems’, The First International Conference on Collaborative Computing: Networking, Applications and Worksharing (CollaborateCom 2005), 2005.
  • Lin, K., Chen, D., Sun, C., Dromey, R.G., ‘A constraint maintenance strategy and applications in real-time collaborative environments’, The Second International Conference on Cooperative Design, Visualization and Engineering (CDVE2005), 2005.
  • Lin, K., Chen, D., Dromey, R.G., Xia, S., Sun, C., “API design recommendations for facilitating conversion of single-user applications into collaborative applications”, 3rd International Conference on Collaborative Computing: Networking, Applications and Worksharing, November 2007.
  • Lin, K., Chen, D., Sun, C., Dromey, R.G., “Leveraging single-user Microsoft Visio for multi-user real-time collaboration”, Proceedings 4th International Conference Cooperative Design, Visualization, and Engineering, CDVE 2007, September 2007; Lecture Notes in Computer Science, Vol. 4674, 353-360.
  • Lin, K., Chen, D., Sun, C., Dromey, R.G., ‘Maintaining constraints in collaborative graphic systems: the CoGSE approach’, 9th European Conference on Computer-Supported Cooperative Work (ECSCW05), 2005.
  • Lin, K., Chen, D., Sun, C., Dromey, R.G., 'Multi-way dataflow constraint propagation in real-time collaborative systems', Proceedings of the 2nd International Conference on Collaborative Computing: Networking, Applications and Worksharing (CollaborateCom 2006), 2006.
  • Lin, K., Chen, D., Sun, C., Dromey, R.G., "Tree structure maintenance in a collaborative genetic software engineering system", Proceedings of the Sixth International Workshop on Collaborative Editing Systems, 2004.
  • Wen, L., Colvin, R., Lin, K., Seagrott, J., Yatapanage, N., Dromey, R.G., “Integrare, a collaborative environment for behavior-oriented design”, Proceedings 4th International Conference on Cooperative Design, Visualization, and Engineering, September 2007; Lecture Notes in Computer Science, Vol. 4674, 122-131.

Validation and rapid prototyping for Behavior Trees

Project Leaders: Geoff Dromey, Ian Hayes
Researchers: Sameer Alam, Robert Colvin, Diana Kirk, Toby Myers, Lian Wen,

Simulation and animation are techniques for quickly obtaining a dynamic, visual view of a system from a high-level specification. This may be useful for receiving feedback from a client early in the software life-cycle (validation), or for demonstrating the behaviour of a model which is difficult to observe statically (in particular, emergent behaviour). This project developed simulation and animation tools for the Behavior Tree framework.

A simulation and model-checking tool began development in 2005. The tool is being developed in Mercury, a declarative programming language similar to Prolog. The high-level nature of Mercury meant that there was a straightforward translation of the semantics of the Behavior Tree process algebra into an executable format. Mercury's backtracking facility also allows the tool to act as a simulator (able to give a particular run of a system), as well as exhaustively produce all possible runs of a system.

In 2006, a Behaviour Tree editing tool was developed, incorporating several different tools and allowing them to exchange information. The tool also has a collaborative mode where users can work on the same tree in real-time. The simulation tool was integrated with the editing tool Integrare, giving a graphical interface to the simulation. A Behavior Tree Framework for Implementation utilising code generation began development in 2006. The Behavior Tree framework can generate code in either Java or C++ using automated code generation from an XML specification of a Behavior Tree.

Foundations of Behavior Trees

Project Leaders: Geoff Dromey, Ian Hayes
Researcher: Robert Colvin

Behavior Trees are a new framework which allows the functional behaviour of a system to be constructed out of its requirements. Behavior Tree notation is easy to learn and use, and can be used to model a wide range of complex systems, including large software systems and biological and chemical processes. This project developed a formal semantics for the Behavior Tree framework, which will help to precisely define and compare systems, and allow automated tool support for the development of software in the framework. The project also extended the Behavior Tree language and semantics to handle real-time and stochastic specifications.

In 2005, a flexible process algebra was designed that can be used to express the majority of Behavior Tree concepts. An operational semantics was defi ned for this language, and a straightforward translation from the high level Behavior Tree notation into the process algebra was developed. The generality of the process algebra fed back into the development of the Behavior Tree notation, resulting in the addition of elegant and powerful specification constructs for the framework as a whole. In 2005 we also developed a metamodel for the core notation of Behavior Trees along similar lines to the UML metamodel.

In 2006, the operational semantics was extended to include more powerful constructs such as generalised nondeterministic choice and parallel choice from a set of components or values, and parameterised message passing. The notation was extended to handle real-time constraints, based on the work of Timed Automata. A prototype tool for translating Behaviour Trees to timed automata, suitable for input to the model checker, UPPAAL, was developed. This work is to be published in ASWEC 2007.

In 2007, progress was made with developing a framework with enough expressive power to formalise the complex  relational behaviour that is often found in large-scale realworld systems. A framework was developed and applied in representing complex behaviour in six large-scale projects. The framework provides a way of structuring and decomposing complex behaviour into fragments that can be individually formalised and then composed. This development should provide a basis for the formalisation necessary to support simulation and model-checking.

In 2008 the semantics for Behavior Trees were redefined as an extension of the well-known process algebra CSP. This is a more mature version of the semantics which opens up the possibility of reusing analysis tools developed for CSP, and the potential for collaboration with other groups. This work won the Best Paper award at the 2009 Integrated Formal Methods Conference. The semantics were also extended to capture relational behaviour, which is a fundamental behavioural type commonly used in requirement documents.

  • Colvin, R., Hayes, I.J., “A semantics for Behavior Trees”, ACCS Technical Report, No. ACCS-TR-07-01, ARC Centre for Complex Systems, April 2007.
  • Colvin, R., Hayes, I.J., “CSP with hierarchical state”, Integrated Formal Methods: 7th International Conference, (IFM), Dusseldorf, Germany, February 2009, 188–35.
  • Dromey, R.G., ‘System composition: Constructive support for the analysis and design of large systems’, Proceedings of the Systems Engineering/Test and Evaluation Conference (SETE 05), 2005.
  • Gonzalez-Perez, C., Henderson-Sellers, B., Dromey, R.G., ‘A metamodel for the Behavior Trees modelling technique’, Proceedings of the 3rd International Conference on Information Technology and Applications (ICITA), 2005.
  • Grunske, L., Winter, K., Colvin, R., 'Timed Behavior Trees and their application to verifying real-time systems', Proceedings of 18th Australian Conference on Software Engineering (ASWEC 2007), April 2007.
  • Grunske, L., Winter, K., Yatapanage, N., “Defining the abstract syntax of visual languages with advanced graph grammars—A case study based on Behavior Trees”’, Journal of Visual Languages and Computing, Vol. 19, No. 3, 2008, 343–79.
  • Winter, K., Colvin, R., Dromey, R.G., “Dynamic relational behaviour for large-scale systems pages”, Australian Software Engineering Conference (ASWEC), 2009.

Model-based development of safety-critical systems

Project Leader: Peter Lindsay
Researchers: Robert Colvin, Geoff Dromey, Lars Grunske, Kirsten Winter, Nisansala Yatapanage, Saad Zafar

The use of model-driven software engineering is steadily growing. In this paradigm engineers work directly with models and computer programs are generated automatically from the models. However the evidence required for system safety assurance currently still has to be derived by hand. This project aimed to develop new methods for automated evaluation of safety properties from models. Specifically the project developed encapsulated models for computer-based systems. The project was funded in part by the Boeing Postdoctoral Research Fellowship Award to the University of Queensland.

In 2005 research focused on failure propagation for component-based software engineering.

In 2006, this project has successfully applied the theoretical concepts of failure propagation models to an embedded control application in the automotive domain. This application was a computer-assisted braking system designed within the component-based development framework SaveCCM. Additionally, progress was made in using model-driven safety evaluation techniques in the optimisation of architecture specifications.

In 2007, we have created an automatic approach for probabilistic FMEA based on probabilistic model checking. This approach has been applied to the case study of an ambulatory infusion pump (medical device). Furthermore, we developed an outline of an architecture based method for optimising dependability attributes of software-intensive systems.

  • Grunske, L., 'Evolutionary algorithms for safety-costs trade-off in control system design', Proceedings of INCOM 2006, 2006, 249-254.Grunske, L., 'Identifying "good" architectural design alternatives with multi-objective optimization strategies', Proceedings of the International Conference on Software Engineering (ICSE), Emerging Results, 2006, 849-852.
  • Grunske, L., ‘Using a graph transformation system to improve the quality characteristics of UML-RT specifications’, Advances in Software Engineering with UML and XML-Based Software Evolution, Idea Group Inc, 2005, 19–45.
  • Grunske, L., 'Towards an integration of standard component-based safety evaluation techniques with SaveCCM', Quality of Software Architectures, 2006; Lecture Notes in Computer Science, Vol. 4214, 199–213.
  • Grunske, L., Colvin, R., Winter, K., “Probabilistic model-checking support for FMEA”, Proceedings of 4th International Conference on the Quantitative Evaluation of SysTems (QEST 2007), 2007, 119-128.
  • Grunske, L., Kaiser, B., ‘Automatic generation of analyzable failure propagation models from component level failure annotations’, 5th International Conference on Quality Software (QSIC), 2005, 117–123
  • Grunske, L., Kaiser, B., Papadopoulos, Y., ‘Modeldriven safety evaluation with state-event-based component failure annotations’, Component-Based Software Engineering: 8th International Symposium, CBSE 2005, February 2005; Lecture Notes in Computer Science, vol. 3412, 33–45.
  • Grunske, L., Kaiser, B., Reussner, R., ‘Specification and evaluation of safety properties in a component based software engineering process’, Embedded System Development with Components, Lecture Notes in Computer Science, vol. 3778, Springer Verlag, 2005, 249 –274.
  • Grunske, L., Lindsay, P., Bondarev, E., Papadopoulos, Y., Parker, D., “An outline of an architecture-based method for optimising dependability attributes of software intensive systems”, Architecting Dependable Systems IV, Lecture Notes in Computer Science, Vol. 4615, Springer, August 2007, 188-209.
  • Maydl, W., Grunske, L., ‘Behavioural types for embedded software - a survey’, Embedded System Development with Components, Lecture Notes in Computer Science, vol. 3778, Springer Verlag, 2005, 82–106.
  • Papadopoulos, Y., Grante, C., Grunske, L., Kaiser, B., ‘Continuous assessment of evolving designs and reuse of analyses in a model-based technique for semi-automatic Fault Tree and FMEA analysis of complex systems’, CD Proceedings IFAC WC 05, 16th World Congress, International Federation of Automatic Control, 2005.
  • Smith, G., Winter, K., “Model checking action system refinements”, Formal Aspects of Computing, 2007.
  • Zafar, S., Colvin, R., Winter, K., Yatapanage, N., Dromey, R.G., “Early validation and verification of a distributed role-based access control model”, 14th Asia-Pacific Software Engineering Conference (APSEC2007), December 2007, Japan, 2007; 430-437.

Verification of lock-free algorithms

Project Leader: Robert Colvin
Researchers: Brijesh Dongol, Lindsay Groves,Ian Hayes, Victor Luchangco, Mark Moir

Computer systems are increasingly being used to tackle problems involving interactions between hundreds of independent processes, all competing for access to some central data store. The algorithms underlying such complex computer systems can be implemented using a new technique, called a ’lock-free’ approach, which provides significant improvements in efficiency over existing implementation techniques. However the benefits come at the cost of increased complexity of the algorithms involved. This project investigated effective strategies for verifying lock-free algorithms, building on earlier work using I/O Automata and simulation techniques.

In 2006, several nonblocking algorithms were formally verified, including a scalable lock-free stack and a lazy wait-free queue. A theory for proving lock-freedom was developed, and this theory was encoded in the PVS theorem prover and applied to two examples.

In 2007, existing research links with Sun Laboratories in Boston, USA, and Victoria University of Wellington, NZ, were strengthened when Dr Colvin visited Sun Laboratories in October. This resulted in expanding the collaboration to include researchers at MIT, Naval Research Laboratories, and a private company, whose specification and verification tools will be used by the project in 2008.

In 2008 a new technique for proving lock-freedom was developed. It is simpler and more general than earlier techniques. The technique was successfully applied to more complex algorithms.

  • Colvin, R., Dongol, B., “A general technique for proving lock-freedom”, Science of Computer Programming, Vol. 74, No. 3, 2009, 143–65.
  • Colvin, R., Dongol, B., “Verifying lock-freedom using well-founded orders”, The 4th International Colloquium on Theoretical Aspects of Computing; Lecture Notes in Computer Science, Vol. 4711, 2007, 124-138.
  • Colvin, R., Groves, L., “A scalable lock-free stack algorithm and its verification”, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), September 2007, London, UK, 339-348.
  • Groves, L., Colvin, R., “Derivation of a scalable lock-free stack algorithm”, Electronic Notes Theoretical Computer Science, Vol. 187, 2007, 55-74.
  • Colvin, R., Groves, L., Luchangco, V., Moir, M., 'Formal verification of a lazy concurrent list-based SetAlgorithm', CAV, 2006, 475-488.
  • Dongol, B., 'Formalising progress properties of non-blocking algorithms', 8th International Conference on Formal Engineering Methods, 2006; LNCS, Vol. 4260, 284-303.
  • Dongol, B., Hayes, I., “Enforcing safety and progress: An approach to concurrent program derivation”, Australian Software Engineering Conference (ASWEC), 2009.

Quantitative modelling and analysis of critical systems with Behavior Trees

Project Leaders: Lars Grunske, Kirsten WInter
Researchers: Robert Colvin, Peter Lindsay, Kirsten Winter

Complex systems often exhibit real-time and stochastic behaviour. To analyse requirements of such systems a modelling notation is needed to capture timing and probabilistic constraints. This also needs to be supported by tools for automated analysis.

In 2007, the Behavior Tree notation was extended to express both real-time and probabilistic behaviour. An existing tool was also extended with an interface supporting the use of the graphical notation of Behavior Trees. We applied our approach to case studies that were derived from the requirements of medical equipment.

In 2008 the project conducted further studies using stochastic analysis tools. We investigated the combined use of the simulator Modelica and the stochastic analysis tool PRISM in the context of safety analysis, in particular in the process of Failure Modes and Effects Analysis (FMEA). This study resulted in a new methodology for hazard identification and tool supported quantitative FMEA. Moreover, the insight into the techniques supported by the PRISM tool led to a translation scheme from probabilistic Behavior Trees to the PRISM input notation. This translation scheme will be implemented to provide automated support for analysing probabilistic Behavior Trees.

  • Colvin, R., Grunske, L., Winter, K., “Probabilistic timed Behavior Trees.”, Proceedings of 6th International Conference on Integrated Formal Methods (IFM 2007), 2007; Lecture Notes in Computer Science, Vol. 4591, 156-175.
  • Colvin, R., Grunske, L., Winter, K., “Timed Behavior Trees for failure mode and effects analysis of time-critical systems”, Journal of Systems and Software, Vol. 81, No. 12, 2008, 2163–82.
  • Grunske, L., Winter, K., Colvin, R., “Timed Behavior Trees and their application to verifying real-time systems”, Proceedings of 18th Australian Conference on Software Engineering (ASWEC 2007), April 2007.
  • Gawanmeha, A., Tahara, S., Winter, K., “Formal verification of ASMs using MDGs”, Journal of Systems Architecture, Vol. 54, No. 1–2, 2008, 15–34.
  • Smith, G., Winter, K., “Model checking action system refinements”, Formal Aspects of Computing, Vol. 21, No. 1, 2009, 155–86.
  • Zafar, S. Colvin, R., Winter, K., Yatapanage, N., Dromey, R.G. “Early validation and verification of a distributed role-based access control model”. 14th Asia-Pacific Software Engineering Conference, Nagoya, Japan, December 2008. 430–37.

Analysing the requirements for large-scale software-integrated systems

Project Leaders: Danny Powell, Terry Stevenson
Researchers: Jim Boston, Geoff Dromey, John Seagrott

This project was designed to assess the effectiveness of using the analysis method we have developed using Behavior Trees and Composition Trees for modelling and finding major defects in acquisition and functional performance requirements documentation for large-scale industry projects. The requirements documentation for six large projects were analysed, each involving approximately 1000 requirements. In each case the analysis was carried out after normal reviews and inspections had been conducted and after the defects found by these methods had been corrected. The project was largely funded by Raytheon Australia.

A major outcome of this work in 2007 has been that across all projects we found on average an additional 130 major (confirmed) defects/1000 requirements after normal reviews and corrections had been made. The early detection and resolution of such defects translates into substantial cost savings on a project — without this analysis intervention these defects would have fl owed through to later stages of the project where their impact would have escalated project costs. What is also important is that the cost of finding a defect is roughly $70 and it takes only about 100 hours to analyse 1000 requirements. Feedback from one project manager was as follows: “I see it as a key risk mitigation strategy, of use in both solution development and as a means of advising the customer on problems with the acquisition documentation. Our team now has a strong understanding of the FPS, at the cost of a relatively small investment. Whilst similar results could have been achieved using conventional processes, the cost and time involved would have been far greater”. These industry trial results provide strong evidence for the scaleability and effectiveness of the method.

Raytheon Australia has provided the funding to develop an industrial strength modelling tool based on the DCS team’s prototype. This tool became available in January 2008. Raytheon Australia is moving to adopt the method as part of their standard process. Raytheon Company (73 000 employees) is about to start evaluation trials with use of the method and Raytheon Australia will be employing the method on one of Australia’s largest projects. Currently we are also conducting trials with other companies and the Queensland Education Department.

  • Boston, J., “Behavior Trees—How they improve engineering behaviour”, 6th Annual Software and Systems Engineering Process Group Conference (SEPG), Melbourne, August. 2008.
  • Powell, D., “Requirements evaluation using Behavior Trees – Findings from industry”, Australian Software Engineering Conference (ASWEC’07), Melbourne, April, 2007.

General DCS publications

  • Colvin, R., Hayes, I.J., Strooper, P., “Calculating modules in contextual logic program refinement”, Theory and Practice of Logic Programming, Vol. 8, No. 01, 2008, 1–31.
  • Dromey, R.G., 'Climbing over the 'no silver bullet' brick wall', IEEE Software, Vol. 23, No. 2, March 2006, 118-120.
  • Dromey, R.G., “Engineering large-scale systems—Mitigating the pivotal risks”, Unpublished report, www.behaviorengineering.org/images/publications/dromey2/eng-large-scale-dec-2008.doc 2008.
  • Dromey, R.G., 'Making real progress with the requirements defect problem', Measuring Quality Requirements in Information Systems, Idea Group Inc, 2006, 87-108.
  • Dromey, R.G., “Taming complexity in large scale systems”, Outcomes. Results of Research in the Real World, Australian Research Council, 2008, 28–31.
  • Jones, C., Hayes, I.J., Jackson, M., “Deriving specifications for systems that are connected to the physical world”, Formal Methods and Hybrid Real-Time Systems, Lecture Notes in Computer Science, Vol. 4700, Springer, 2008.
  • Phillips, V., “Implementing a Behavior Tree analysis tool using Eclipse development frameworks”, Australian Software Engineering Conference (ASWEC), Perth, March 2008.
  • Sithirasenan, E., Zafar, S., Muthukkumarasamy, V., 'Formal verification of the IEEE 802.11i WLAN security protocol', Australian Software Engineering Conference (ASWEC '06), 2006, 181-190.
  • Smith, G., Winter, K., 'Simulation machines for checking action system refinements', REFINE 2006 - International refinement workshop, 2006; Electronic Notes in Theoretical Computer Science.
World-class basic and applied inter-disciplinary research on questions fundamental to understanding, designing and managing complex systems
© 2009 The ARC Centre for Complex Systems, Australia