title page
Abstract
Contents
Abbreviations 10
I. Introduction 11
1.1. Motivation 11
1.2. Contribution 12
1.3. Outline 12
II. The Related Works 14
2.1. Architectural View 14
2.2. FSP Model and LTSA 20
2.3. ADL 27
2.4. Implementing System from Architecture 28
2.5. Synthesized Algorithm 29
III. An Approach To verify C&C view Architecture with FSP Modeling 31
3.1. An Approached Steps 31
3.2. A Simple Example 33
3.2.1. Describing C&C View Architecture 33
3.2.2. Creating MSC 35
3.2.3. Creating Statechart and FSP model 37
3.2.4. Check System's Behavioral Property with LTSA 40
IV. An Application Example 43
4.1. Describing C&C view architecture 44
4.2. Creating MSC 51
4.3. Describing Statechart and FSP Model 52
4.4. Check system behavioral property with LTSA 56
V. Conclusion 59
국문 요약 61
References 63
감사의 글 68
Curriculum Vitae 70
FIGURE 1. An example of C&C view architecture 18
FIGURE 2. an FSP model and its stage diagram 21
FIGURE 3. A simple example of LTS 24
FIGURE 4. Safety analysts performed by LTSA in simple safety example. 25
FIGURE 5. A simple example of safety property 25
FIGURE 6. A sample example of COIN model for verifying liveness property 26
FIGURE 7. The approached step for checking system's behavior 31
FIGURE 8. Architecture of the example system 34
FIGURE 9. Message sequence cart of Login 35
FIGURE 10. Message sequence chart of Logout 36
FIGURE 11. Statechart of LoginMgr component 37
FIGURE 12. Statechart of EventBus connector 38
FIGURE 13. Statechart of LoggingMgr component 39
FIGURE 14. The composition of a example system with LTSA 40
FIGURE 15. The result of FSP property check with LTSA 42
FIGURE 16. Business Context Diagram of TestGen 44
FIGURE 17. C&C view of translator 47
FIGURE 18. A sequence chart for the translator system. 51
FIGURE 19. The state diagram of Main_Controller 52
FIGURE 20. The state diagram of Parser 53
FIGURE 21. The state diagram of Code_Gen 54
FIGURE 22. The state diagram of Symbol_Table 55
FIGURE 23. FSP property check in application system 57