第1页 / 共111页
第2页 / 共111页
第3页 / 共111页
第4页 / 共111页
第5页 / 共111页
第6页 / 共111页
第7页 / 共111页
第8页 / 共111页
LTSA以及FSP语言相关介绍.pdf
Validation and Verification of
Software Design
Using Finite State Process
by
Simon C. Stanton, B. Sc.
A dissertation submitted to the School of Computing in partial fulfilment of the
requirements for the degree of Bachelor of Science with Honours
University of Tasmania
November 2002
I, Simon Charles Stanton, declare that this thesis contains no material which has
been accepted for the award of any other degree or diploma in any tertiary
institution. To my knowledge and belief, this thesis contains no materials
previously published or written by another person except where due reference is
made in the text of the thesis.
Simon Charles Stanton
ii
Abstract
This thesis aims to evaluate the effectiveness, at eliminating errors from a design
specification, of a formal language (Finite State Process) automated verification
tool (Labelled Transition System Analyser). The language FSP is used to model
the problem domain (a version of the Lift Problem), based on a provided
specification that was refined with a validation-led methodology. The validation-
led model is translated (mapped) to a finite state domain wherein we test this new
model for errors in the translation, for errors in the understanding of the initial
requirements, and for faults in the concurrency properties of the identified co-
operating entities. Exposition of errors drives their resolution. The resolution of
errors gives rise to an evolutionary corrected model. The corrected model is then
used as a specification for input to Implementation phases of software engineering,
or, the corrected model may be used as input back to the client as text descriptions.
Input returning to the client validates the problem solution, enabling a new cycle
of modelling and design. Performing a documented process of FSP modelling
over the evolutionary descriptions brings to light some issues that suggest the
inclusion of formal methods in the design process has value due to the early
removal of errors. Specifically, fatal errors, non-fatal errors and contributory
specifications have all been explicitly realised from the FSP process - allowing
the assertion that the formal method examined in this thesis assists the software
engineering process.
iii
Acknowledgements
Vishv Malhotra, for his support, instruction and guidance throughout the year,
Phaedra, for living with a thesis,
Julian Dermoudy for his help and encouragement,
All the honours students, for being there,
Debbie Ploughman for proofreading,
Ian Cumming, Frank Sainsbury and Jonathan Elliott for their help and assistance
with blizzard, and
TPAC (Tasmanian Partnership for Advanced Computing) for access to blizzard,
SGI Origin 3400.
iv
Table of Contents
1 Introduction.......................................................................................................1
1.1 Software Engineering Models ............................................................................. 1
1.2 Error Generation Phases ..................................................................................... 1
1.3 Validation-led Development ................................................................................ 2
1.4 Validation of Software Design using Finite State Process ................................ 2
1.4.1 Case Study: The Lift Problem......................................................................................3
1.4.2 Implementation Specification ......................................................................................3
1.5 Overview of Thesis ............................................................................................... 4
2 Theory Review and Current Work....................................................................5
2.1 Finite State Process and the Labelled Transition System Analyser................. 5
2.1.1 Finite State Process ......................................................................................................6
2.1.2 Labelled Transition System Analyser ..........................................................................6
2.1.3 FSP Modelling of Concurrent Processes......................................................................7
2.1.4 Verification using LTSA..............................................................................................8
2.1.5 The Darwin Architectural Language............................................................................9
2.2 Architectural Description Languages............................................................... 10
2.3 Software Development Lifecycles ..................................................................... 12
2.4 The Unified Modelling Language and Software Architecture ....................... 13
2.4.1 UML...........................................................................................................................13
2.4.2 Software Architectures...............................................................................................14
2.5 Formal Descriptions and Verification .............................................................. 15
2.6 Validation-Led Development............................................................................. 17
3 Research Question...........................................................................................19
3.1 Software Engineering Model............................................................................. 20
3.1.1 Client Description ......................................................................................................20
3.1.2 Developer Model........................................................................................................20
3.2 Error Generation and Removal ........................................................................ 21
3.3 Validation-led Development .............................................................................. 21
v
3.4 Validation of Software Design using Finite State Process .............................. 22
3.4.1 Client Description ......................................................................................................22
3.4.2 Developer Model........................................................................................................23
3.4.2.1 Transition ID ......................................................................................................23
3.4.2.2 Current State.......................................................................................................23
3.4.2.3 Event...................................................................................................................23
3.4.2.4 Guard..................................................................................................................23
3.4.2.5 Actions ...............................................................................................................24
3.4.2.6 Next State ...........................................................................................................24
3.4.3 Implementation Specification ....................................................................................24
3.4.4 Error Removal through Iteration ................................................................................24
3.4.5 Description – Model – Analysis Cycle.......................................................................25
3.4.6 Corrected Model.........................................................................................................25
3.5 Pre-FSP Object Model ....................................................................................... 26
3.6 Summary of Research Question........................................................................ 26
4 Problem Statement ..........................................................................................28
4.1 Apply FSP to a Case Study Problem ................................................................ 28
4.2 Case Study: The Lift Problem........................................................................... 28
5 Research Process.............................................................................................30
5.1 Development of Lift System using FSP............................................................. 30
5.1.1 Identification of Components.....................................................................................31
5.1.2 Development of pre-FSP Object Model.....................................................................32
5.1.3 Modelling components in FSP ...................................................................................33
5.1.4 Composition of Individual Elements..........................................................................34
5.1.5 Test Model using LTSA.............................................................................................35
5.1.6 Remodelling of Components......................................................................................36
5.1.7 Composition, Relabelling and Hiding........................................................................38
5.1.8 Documentation and Iteration......................................................................................39
5.1.9 Corrected Model Exit Conditions...............................................................................39
5.2 Evaluation of Error Documentation................................................................. 40
5.2.1 Analysis errors ...........................................................................................................40
5.2.2 Model Errors ..............................................................................................................42
5.2.3 Description Errors ......................................................................................................44
5.3 Corrected Model to Implementation Specification ......................................... 45
5.3.1 The Walk Algorithm ..................................................................................................51
5.3.2 Implicit Transitions ....................................................................................................53
vi
5.4 Corrected Model to Developer Model .............................................................. 53
5.4.1 Lift object errors revealed in Developer Model .........................................................53
5.4.1.1 Fatal concurrency flaws in developer model......................................................54
5.4.1.2 Non-fatal concurrency flaws in developer model...............................................54
5.4.1.3 Contributory specifications ................................................................................54
5.5 Corrected Model to Client Description ............................................................ 55
6 Implementation Details ...................................................................................57
6.1 Further Optimisations........................................................................................ 57
6.2 Dependencies....................................................................................................... 57
6.3 Derivation of Lift Problem Description............................................................ 58
6.3.1 Abstraction of Lift Controller ....................................................................................58
6.3.2 Timing Issues .............................................................................................................58
6.4 Passengers ........................................................................................................... 59
6.4.1 Well Behaved Passengers...........................................................................................59
6.5 Atomic Walks...................................................................................................... 59
6.6 Tight Coupling of FSP Processes ...................................................................... 60
6.7 Separation of Components in UML Model ...................................................... 60
7 Research Discussion........................................................................................61
7.1 Summary of Methodology ................................................................................. 61
7.2 The Implementation Specification and pre-FSP Object Models.................... 61
7.3 State Space and Computational Limits ............................................................ 62
7.4 Well-Behaved Passengers and other Constraints............................................ 63
8 Conclusion.......................................................................................................64
9 Further Work...................................................................................................66
9.1 Optimisations on Implementation Specification.............................................. 66
9.2 Development of Architectural Description....................................................... 66
10 References......................................................................................................67
11 Appendix ........................................................................................................69
11.1 Original Case Study - The Lift Problem ........................................................ 69
11.2 Validation-Led Specifications.......................................................................... 70
vii
11.3 Early stage FSP Listing for a Lift (Section 5.1.3) .......................................... 74
11.4 Early FSP Listing Passenger ........................................................................... 77
11.5 Error Documentation Summary ..................................................................... 78
11.6 State-Space Data............................................................................................... 83
11.7 LIFT_SYSTEM_SAFE.lts ............................................................................... 84
viii
相关推荐
2023年江西萍乡中考道德与法治真题及答案.doc
2012年重庆南川中考生物真题及答案.doc
2013年江西师范大学地理学综合及文艺理论基础考研真题.doc
2020年四川甘孜小升初语文真题及答案I卷.doc
2020年注册岩土工程师专业基础考试真题及答案.doc
2023-2024学年福建省厦门市九年级上学期数学月考试题及答案.doc
2021-2022学年辽宁省沈阳市大东区九年级上学期语文期末试题及答案.doc
2022-2023学年北京东城区初三第一学期物理期末试卷及答案.doc
2018上半年江西教师资格初中地理学科知识与教学能力真题及答案.doc
2012年河北国家公务员申论考试真题及答案-省级.doc
2020-2021学年江苏省扬州市江都区邵樊片九年级上学期数学第一次质量检测试题及答案.doc
2022下半年黑龙江教师资格证中学综合素质真题及答案.doc
