Peter A. Lindsay
University of Queensland
Reliability engineeringSystems engineeringComputer scienceSoftware developmentFormal methods
What is this?
Publications 103
#1Peter A. Lindsay (UQ: University of Queensland)H-Index: 16
#2Sentot Kromodimoeljo (UQ: University of Queensland)H-Index: 1
Last. Mohamed Almorsy (Swinburne University of Technology)H-Index: 9
view all 4 authors...
Behavior Trees (BTs) are a graphical notation for requirements capture that is easier to read than other formal notations, with direct traceability between individual functional requirements and their representation in the BT model. This paper investigates whether this relationship can be extended to generation of test cases, using a symbolic model checker to ensure correctness and completeness of test cases with respect to the model. To do so it was necessary to provide mechanisms for test plan...
#1Sentot Kromodimoeljo (UQ: University of Queensland)H-Index: 1
#2Peter A. Lindsay (UQ: University of Queensland)H-Index: 16
A cut set is a collection of component failure modes that could lead to a system failure. Cut Set Analysis (CSA) is applied to critical systems to identify and rank system vulnerabilities at design time. Model checking tools have been used to automate the generation of minimal cut sets but are generally based on checking reachability of system failure states. This paper describes a new approach to CSA using a Linear Temporal Logic (LTL) model checker called BT Analyser that supports the generati...
2 CitationsSource
#1Mike HincheyH-Index: 32
#2Bernd KleinjohannH-Index: 12
Last. Marilyn WolfH-Index: 1
view all 7 authors...
st This volume contains the proceedings of two conferences held as part of the 21 IFIP World Computer Congress in Brisbane, Australia, 2023 September 2010. th The first part of the book presents the proceedings of DIPES 2010, the 7 IFIP Conference on Distributed and Parallel Embedded Systems. The conference, int- duced in a separate preface by the Chairs, covers a range of topics from specification and design of embedded systems through to dependability and fault tolerance. rd The second part of...
#1Shane D. Arnott (UQ: University of Queensland)H-Index: 1
#2Peter A. Lindsay (UQ: University of Queensland)H-Index: 16
Defense Experimentation (DE) using modeling and simulation (M&S) is increasingly being adopted as a means to better understand complex defense capability problems. This is being given added impetus by the amplified focus on Network Enabled Capability (NEC) and the rising use of advanced information and communications technology within military operations. This paper presents analysis of observed data trends from a broad range of DE experiments performed within capability development programs for...
1 CitationsSource
#1Soon-Kyeong KimH-Index: 1
#2Toby Myers (Griffith University)H-Index: 4
Last. Peter A. Lindsay (UQ: University of Queensland)H-Index: 16
view all 4 authors...
This paper defines a transformation from Behavior Tree models to UML state machines. Behavior Trees are a graphical modelling notation for capturing and formalising dynamic system behaviour described in natural language requirements. But state machines are more widely used in software development, and are required for use with many tools, such as test case generators. Combining the two approaches provides a formal path from natural language requirements to an executable model of the system. This...
6 CitationsSource
#1Peter A. Lindsay (UQ: University of Queensland)H-Index: 16
#2Nisansala Yatapanage (Griffith University)H-Index: 7
Last. Kirsten Winter (UQ: University of Queensland)H-Index: 17
view all 3 authors...
Safety analysis can be labour intensive and error prone for system designers. Moreover, even a relatively minor change to a system’s design can necessitate a complete reworking of the system safety analysis. This paper proposes the use of Behavior Trees and model checking to automate Cut Set Analysis (CSA) : that is, the identification of combinations of component failures that can lead to hazardous system failures. We demonstrate an automated incremental approach to CSA, in which models are ext...
8 CitationsSource
#1Peter A. Lindsay (UQ: University of Queensland)H-Index: 16
#2Kirsten WinterH-Index: 17
Last. Sentot KromodimoeljoH-Index: 1
view all 3 authors...
For complex engineered systems, it is important to conduct technical risk assessment early in the system development life-cycle, in order to identify critical system requirements, such as safety requirements, that should be included in design. This paper proposes a model-based approach to such assessment, which can be applied from the system requirements analysis stage onwards. The approach starts with the application of the Behaviour Trees modelling notation to natural language functional requi...
#1Peter A. LindsayH-Index: 16
#1Lars Grunske (Swinburne University of Technology)H-Index: 30
#2Kirsten Winter (UQ: University of Queensland)H-Index: 17
Last. Peter A. Lindsay (UQ: University of Queensland)H-Index: 16
view all 5 authors...
Failure Modes and Effects Analysis (FMEA) is a widely used system and software safety analysis technique that systematically identifies failure modes of system components and explores whether these failure modes might lead to potential hazards. In practice, FMEA is typically a labor-intensive team-based exercise, with little tool support. This article presents our experience with automating parts of the FMEA process, using a model checker to automate the search for system-level consequences of c...
23 CitationsSource
#1Cliff B. JonesH-Index: 33
#2Kevin D. JonesH-Index: 6
Last. Richard MooreH-Index: 3
view all 4 authors...
syntax In Extended BNF (Backus-Naur Form), the syntax is roughly: Term = Exp | Type Exp = VSymb | CESymb{Exp}{Type} | DESymb VSymb‘:’Type‘·’Exp Type = CTSymb{Exp}{Type} | DTSymb VSymb‘:’Type‘·’Type | ‘ ’ In other words, expressions are built up from variables using two kinds of combinators: • compound expressions, whereby a constant is ‘applied’ to (possibly empty) lists of expressions and types (called its operands, or ‘arguments’);1 • binder expressions, whereby a binder is supplied with a dum...
4 Citations