of
Software Architectural Style
M.Tech. (Research) THESIS
by
ASHISH KUMAR DWIVEDI
Department of Computer Science and Engineering National Institute of Technology Rourkela
Rourkela- 769008, India JUNE 2014
of
Software Architectural Style
Thesis submitted in partial fulfillment of the requirements for the degree of
Master of Technology (Research)
in
Computer Science and Engineering
by
Ashish Kumar Dwivedi
(Roll: 611CS105) under the guidance of
Prof. Santanu Kumar Rath
&
Prof. Durga Prasad Mohapatra
Department of Computer Science and Engineering National Institute of Technology Rourkela
Rourkela- 769008, India 2014
Rourkela-769 008, India.
www.nitrkl.ac.inJune 16, 2014
Certificate
This is to certify that the work in the thesis entitled “Formalization and Model Checking of Software Architectural Style” byAshish Kumar Dwivedi is a record of an original research work carried out by him under our supervision and guidance in partial fulfilment of the requirements for the award of the degree of Master of Technology (Research) inComputer Science and Engineering. Neither this thesis nor any part of it has been submitted for any degree or academic award elsewhere.
(Durga Prasad Mohapatra) (Santanu Kumar Rath)
Associate Professor Professor
The famous English poet in Stratford-upon-Avon said “Pupil Thy Work is Incomplete, till thee thank the Lord and thy Master”, which means a students work is incomplete until he thanks the Almighty and his Teacher. I sincerely believe in this. I sincerely thank God for showing me the right direction.
I would like to express my indebted thanks to my supervisor Prof. S. K.
Rath, for his invaluable guidance, and encouragement during the course of this thesis. His keen interest, patient hearing and constructive criticism have instilled in me the spirit of confidence to successfully complete this thesis. I am greatly indebted for his help throughout the thesis work.
I am grateful to my co-supervisor, Prof. D. P. Mohapatra who has provided me with continuous encouragement and support to carry out research.
I am very much indebted to the Master Scrutiny Committee (MSC) mem- bers Prof. S. K. Jena, Prof. A. K. Turuk, Prof. B. Majhi, Prof. S. Chinara, and Prof. P. Singh for their time to provide more insightful opinions into my research. Besides that, I am also thankful to all the Professors and faculty members of the department for their in time support, advise and encourage- ment.
I am really thankful to all my fellow research colleagues for their cooper- ation. My sincere thanks to Shashank, Prashant, Swati, Suresh, Amar, Lov, Shakya for their all support and help. I am truly indebted.
Most importantly, none of this would have been possible without the love and patience of my family. My family to whom this dissertation is dedicated to, has been a constant source of love, concern, support and strength all these years. I would like to express my heart-felt gratitude to them.
(Ashish Kumar Dwivedi)
implementation of any safety critical system. As the complexity of software increases, the need for reasoning about correct behavior becomes more promi- nent. Algorithmic analysis of different programs is usually carried out in order to prove their properties of execution. Application of formal method is being considered necessary for modeling, verification, and development of any soft- ware or hardware systems. In the formal verification of behavioral model, an attempt has been made to formally describe a real-time system e.g., use of Automated Teller Machine (ATM) in Banks. In this thesis, formal models of ATM system are described using state-based languages such as, Z, B, and Alloy as well as event-based language such as, Monterey Phoenix. Model checking is being carried out by automated tools, viz. Z/EVES, Atelier B, and Alloy Analyzer for Z, B, and Alloy specifications respectively. Furthermore, a com- parative analysis of different characteristics shown by varied formal approaches has been presented in this thesis.
Software architecture plays an important role in the high level design of a system in terms of components, connectors, and configurations. The main building block of software architecture is an architectural style that provides domain specific design semantics. In the analysis of complex architectural style, an attempt has been made in our work to formalize one complex style e.g., C2 (component and connector) using formal specification language Alloy.
For consistency checking of modeling notations, the model checker tool e.g., Al- loy Analyzer is used. Alloy Analyzer automatically checks properties such as, compatibility between components and connectors, satisfiability of predicates over the architectural structure, and consistency of an architectural style. For modeling and verification of C2 architectural style, one case study on Cruise Control System has been considered. At the end of this study, performance evaluation of different SAT solvers associated with Alloy Analyzer has been performed in order to assess the quality.
Keywords: Formal methods, formal verification, model checking, Z, B, Al- loy, Z/EVES, Atelier B, Alloy Analyzer, SAT, Monterey Phoenix, software architecture, and architectural style.
Certificate iii
Acknowledgement iv
Abstract v
List of Acronyms / Abbreviations viii
List of Figures ix
List of Tables xi
List of Symbols xii
1 Introduction 1
1.1 Formal Methods . . . 1
1.1.1 Benefits of Formal Methods . . . 3
1.1.2 Application of Formal methods . . . 4
1.2 Model Checking . . . 4
1.2.1 Model Checking Process . . . 5
1.2.2 Application of Model Checking . . . 5
1.3 Motivation . . . 6
1.4 Objective . . . 7
1.5 Organization of Thesis . . . 7
2 Basic Concepts 9 2.1 Introduction . . . 9
2.2 Formal Modeling Language Z . . . 9
2.2.1 Z Notation . . . 10
2.2.2 Tools Support for Z Language . . . 11
2.3 Formal Modeling Language B . . . 12
2.3.1 B Notation . . . 12
2.4.2 Tools Support for Alloy Language . . . 16
2.5 Modeling Language Monterey Phoenix . . . 16
2.5.1 Event Grammar Rules for Monterey Phoenix . . . 18
2.6 Cruise Control System (CCS) . . . 18
2.7 Architectural Style C2 . . . 20
2.8 Conclusion . . . 22
3 Literature Survey 23 3.1 Introduction . . . 23
3.2 Formalization of Behavioral Models . . . 23
3.3 Model Checking of Software Architectural Styles . . . 25
3.4 Conclusion . . . 28
4 Formal Verification of Behavioral Model 29 4.1 Introduction . . . 29
4.2 Formal Specification using Z . . . 31
4.3 Formal Specification using B . . . 35
4.4 Formal Specification using Alloy . . . 38
4.5 Formal Modeling using Monterey Phoenix . . . 42
4.6 Comparison of Different Formal Methods . . . 44
4.7 Conclusion . . . 46
5 Model Checking of a Complex Architectural Style C2 47 5.1 Introduction . . . 47
5.2 Application of C2 Style on a Case Study . . . 49
5.3 Representing C2 Style of Cruise Control System using Alloy . . 51
5.4 Analysis of Dynamic Behavior of C2 Style . . . 57
5.5 Performance Evaluation among Different SAT Solvers . . . 63
5.6 Conclusion . . . 67
6 Conclusions 68 6.1 Formalization of Behavioral Model . . . 69
6.2 Model Checking of a Complex Architectural Style C2 . . . 69
6.3 Scope for Further Research . . . 70
Bibliography 71
Dissemination 80
Abbreviations
AA Alloy Analyzer
ADL Architectural Description Language ASM Abstract State Machine
ATM Automated Teller Machine C2 Component and Connector CCS Cruise Control System
C2SADEL Software Architecture Description and Evolution Language for C2 CORBA Common Object Request Broker Architecture
CPN Coloured Petri Nets
CSP Communicating Sequential Process
LOTOS Language Of Temporal Ordering Specification OCL Object Constraint Language
MP Monterey Phoenix
PROMELA PROcess MEta LAnguage UML Unified Modeling Language
RAISE Rigorous Approach to Industrial Software REST REpresentational State Transfer
RoZ Rosette
RSA Rational Software Architecture RSL RAISE Specification Language VDM Vienna Development Method
VHDL VHSIC Hardware Description language VHSIC Very High Speed Integrated Circuits SDL Specification and Description Language SMV Symbolic Model Verifier
SPIN Simple Promela INterpreter
1.1 Schematic view of the model-checking process . . . 5
2.1 Basic type definition using Z notation . . . 10
2.2 Axiomatic definition using Z notation . . . 11
2.3 Schema definition using Z notation . . . 11
2.4 Abstract state machine representation using B notation . . . 13
2.5 Alloy notation for ATM system . . . 15
2.6 Rules of ordering of events using IN and PRECEDES . . . 17
2.7 Class diagram of Cruise Control System . . . 19
2.8 An example of C2 style . . . 21
4.1 Statechart diagram of ATM system . . . 30
4.2 Basic type definition of ATM using Z . . . 31
4.3 Axiomatic definition of ATM using Z . . . 32
4.4 CardReader schema using Z . . . 32
4.5 BalanceEnquiry schema using Z . . . 33
4.6 CashWithdraw schema using Z . . . 34
4.7 Syntax and type checking using Z/EVES tool . . . 34
4.8 Modeling of ATM system using B . . . 36
4.9 Refinement of withdraw cash and transfer fund operations . . . 37
4.10 Formal Verification of ATM system using Atelier B . . . 38
4.11 Alloy model of ATM system . . . 39
4.12 Alloy model of balance enquiry and withdrawal operations . . . 40
4.13 Instances generated by Alloy Analyzer . . . 41
4.14 Phoenix schema of ATM system . . . 42
4.15 Event traces of ATM for ATM Machine schema . . . 43
5.1 Cruise Control System in C2 architectural style . . . 50
5.2 Alloy specification of architectural elements . . . 52
5.3 Alloy specification of sensor components . . . 54
5.4 Alloy specification of artist components . . . 55
5.5 Alloy specification of actuators and controller components . . . 56
5.9 Consistency checking of Cruise Control System . . . 60 5.10 Consistency checking of C2 style . . . 61 5.11 Instances generated by Alloy Analyzer . . . 62 5.12 Meta model of Alloy specification generated by Alloy Analyzer . 64 5.13 Performance evaluation of SAT4J Solver . . . 65 5.14 Performance evaluation among different SAT Solvers . . . 66
1.1 Comparison of Formal Methods on the basis of associated At- tributes . . . 3 4.1 Comparison among Z, B, Alloy, and Monterey Phoenix . . . 45 5.1 Comparative analysis among different SAT Solvers . . . 65
∧ Conjunction
∨ Disjunction
dom Domain of Relation in Z
<: Domain Restriction in Alloy
▹ Domain Restriction in Z
⇔ Equivalence
∅ Empty Set in Z
∃ Existential Quantifier
⇒ Implication
̸
= Inequality
? Input Symbol for Z 7→ Maplet Function in Z
∈ Membership
¬ Negation
Ξ No State Change in Z Schema
# Number of Members of a Set in Alloy
! Output Symbol for Z ++ Override Operator in Alloy
⊕ Override Operator in Z
P Power Set
ran Range of Relation in Z :> Range Restriction in Alloy
◃ Range Restriction in Z
∩ Set Intersection
N Set of Natural Numbers
∪ Set Union
∆ State Change in Z Schema
∀ Universal Quantifier univ Universal Set in Alloy
Introduction
1.1 Formal Methods
Embedded systems emphasize on reliable operation of a product having large social importance. Hence, they need to be properly specified and verified before development using certain formal methods. Formal methods are mathematical approaches, supported by tools and techniques, for verifying essential proper- ties of the desired software or hardware systems. Mathematical techniques and formal logics enable users to specify and verify models of a system at any part of the program life-cycle such as requirements specification, architectural design, implementation, testing, maintenance, and evolution [1]. Formal methods are useful for checking the quality parameters such as correctness, completeness, consistency, traceability, and verifiability of system requirements. A formal model of a system suppresses implementation details during the design phase.
These models are also helpful in fixing the configuration of architectural ele- ments i.e., components and connectors for complex systems. Formal methods are also useful for code verification. According to Hoare, [2] the use of formal assertions in Microsoft are not for program proving, but for testing. An im-
portant role of formal methods is in the maintenance of legacy code. So, for the software development, formal methods are used to specify the semantic relationships of UML (Unified Modeling Language) diagrams.
Software requirements present precisely and unambiguously using a collec- tion of tools and techniques that can capture the abstract features of a system.
The use of a formal modeling languages reduce the ambiguity and ensure the completeness and correctness of the specifications. A Model checker does not check programs, rather than it checks the properties of a model, which are high level descriptions of a system. In order to check whether the modeled system complies with the user requirements, it needs to verify and validate that par- ticular model. Formal modeling is a task to convert a design document into a formal document, which is checked by model checking tools.
Formal methods are mainly associated with three techniques such asformal specification, refinement, and formal verification. Formal specification is used to uncover problems and ambiguities from the system requirements. Many formal specification languages are available in the literature. Some of them are used for sequential systems such as Z [3], B [4], VDM [5], Alloy [6] etc. and others are used for parallel systems such as CSP [7], CPN [8], LOTOS [9], RSL (RAISE Specification Language) [10], Promela [11] etc. For these specification languages, tools such as, Z/EVES [12], Atelier B [13], VDMTools [14] [15], Alloy Analyzer [16] etc. are used for sequential systems and PAT [17], CPNTool [18], LOTOS tool [19], RSL tool [20], SPIN tool [21] etc. are used for parallel systems respectively. The list of formal methods and associated attributes being used for verifying proposed software or hardware are shown in Table 1.1.
These attributes are paradigm, formality, object oriented, concurrency, and tool support. The details about these attributes are mentioned in chapter 4. It is also felt necessary to refine the specification until it can be implemented via a readily verifiable steps. Refinement is an integral part of developing, checking, and verifying the specification. Formal verification is a process to prove or
disprove the correctness of a system with respect to the formal specification or property.
Table 1.1: Comparison of Formal Methods on the basis of associated Attributes
S. No. Methods Paradigm Formality Object Oriented Cuncurrency Tool Support
1 Z State Based Formal No No Yes
2 Object-Z State Based Formal Yes No Yes
3 Alloy State Based Formal Yes No Yes
4 B State Based Formal No No Yes
5 Event-B State Based Formal No No Yes
6 MP Event-Based Formal No Yes No
7 ASM State Based Formal Yes Yes Yes
8 SDL State Based Formal Yes Yes Yes
9 Action Systems State Based Formal No Yes No
10 CSP State Based Formal No Yes Yes
11 LOTOS Process Algebra Formal Yes Yes Yes
12 RAISE Process Algebra Formal Yes Yes Yes
13 Petri Nets State Based Formal No Yes Yes
14 VHDL State Based Semi-Formal No Yes Yes
1.1.1 Benefits of Formal Methods
Formal methods are mainly used in complex and critical systems in order to improve functional and non-functional requirements of a system. There are many advantages of formal methods.
• Formal methods force the System Analyst and Architect to think care- fully about the specification of a system.
• Faults are uncovered that would be missed using informal specification.
• System properties and invariants are preserved by the use of formal proofs.
• Formal methods are mainly used in early phases of the software devel- opment life cycle; hence, they lead to reduce testing and maintenance cost.
• Use of formal methods can improve non-functional requirements such as efficiency, complexity, scalability, adaptability, dependability etc. of a system.
1.1.2 Application of Formal methods
Informal specification of a system needs to be documented and maintained very carefully in order to manage a practical formal verification process. Formal methods are used in several practical Applications.
• Automatic generation of design documents, code generation, and test case generation.
• The largest application area of formal methods was transport, followed by the financial sector [1].
• Other major areas were defence, telecommunications, nuclear sector, con- sumer electronics, embedded systems, and administration.
1.2 Model Checking
Model checking is a formal verification technique based on the exhaustive state space exploration of a finite state machine (FSM). There are a large number of model checkers available such as SPIN [21], PAT [17], SLAM [22], NuSMV [23], TAPPAL [24] etc. for verification process. By model checking, important
system properties like functional behavior, performance characteristic, timing behavior, and consistency of internal structure are verified. Model checking traces its roots to logic and theorem proving. The goal of providing con- ceptual framework is to formalize the fundamental requirements and provide algorithmic procedures for the analysis of logical requirements [25].
1.2.1 Model Checking Process
For verification process model checker considers the formal model of a system and system’s property in the form of logic as input. If property does not hold good then the model checker generates counterexamples. The schematic view of the model-checking process is shown in Figure 1.1.
Figure 1.1: Schematic view of the model-checking process
1.2.2 Application of Model Checking
Model checking is a well-known verification technique which is applied to sev- eral practical applications :
• Verification of hardware systems such as, device drives, chip sets, high end processor verification etc.
• Verification of software.
• Verification of communication and security protocols.
• Consistency checking of reactive systems.
• The main objectives of model checking are analysis, hunting and avoid- ance of bug.
1.3 Motivation
During the development of software architecture, the number of defects grows exponentially with the number of interacting system components. When for- malizing the parameters such as, concurrency and non-determinism, it is ob- served that they are very hard to model using standard designing techniques available in the literature. System’s growing size and complexity, together with the pressure of drastically reducing system development time make the delivery of low-defect systems an enormously challenging and complex activ- ity. Software is used to develop the process control of safety-critical systems such as chemical plants, nuclear power plants, traffic control and alert systems.
Defects in such systems can have disastrous consequences. Apart from these issues there are certain other issues, which have motivated me to carry out research work in the areas of formalization and model checking of software architectural style because of the complexities associated with-
• Functionality issues i.e., growing in size and complexity of a system.
• Non-functional requirement issues such as, efficiency, scalability, avail- ability, reliability, safety, security etc.
• Functional requirement issues i.e., time-to-delivery and costs of project.
• Maintenance issues i.e., requirements changing rapidly over time.
1.4 Objective
Due to the complexity of the present day system, software development process shifted from conventional design techniques to architectural elements such as components and connectors. Hence, it is essential to check the compatibility of an architectural style before the implementation of a system. The objective of the research work as follows:
• To formally verify a behavioral model of any real-time system, different formal modeling languages such as Z, B, Alloy, and Monterey Phoenix have been considered.
• For verification of Z, B, and Alloy specifications, automated tools, viz.
Z/EVES, Atelier B, and Alloy Analyzer are used.
• The compatibility of an architectural style can be verified using proper formal verification techniques such as reachability analysis, automated theorem proving, and model checking etc.
• To formally verify a complex architectural style i.e., C2 (component and connector) a case study has been considered.
• To evaluate the performance among different SAT solvers, a comparison has been made.
1.5 Organization of Thesis
The research work carried out to meet the objective has been organized in the following manner:
Chapter 2 : This chapter provides basic concepts about formal modeling languages considered for formal specification of any real-time system. For verification process different tools supported by these modeling languages have been presented. In this chapter, a safety critical real-time system i.e., Cruise Control System (CCS) is presented. In the last section of this chapter, an
architectural style C2 (Component and Connector) and architectural elements such as component, connector, port, and role are discussed.
Chapter 3 : This chapter provides insight on the state-of-art of various techniques applied for formalization and model checking of real-time systems and different architectural styles. The review has been done in two broad parts with respect to the objectives. The first part describes the formal specification and formal verification of real-time system using different formal modeling languages. The second part describes the modeling and verifying of different architectural styles.
Chapter 4 : In this chapter, behavioral model of a real-time system is formally specified using different formal modeling languages such as Z, B, Alloy, and Monterey Phoenix. Subsequently, it presents the significant information about the effectiveness and weakness of these formal modeling languages as well as the tools supported by these formal languages.
Chapter 5 : In this chapter, an architectural style C2 is modeled using Alloy. For consistency checking of the formal notations, model generator Alloy Analyzer is being used.
Chapter 6 : In this chapter, the work done is summarized, the contri- butions are highlighted and suggestion for the future work has been discussed.
Basic Concepts
2.1 Introduction
A number of formal specification methods have been proposed for the anal- ysis and design of application software. To choose a particular specification method, it depends on the character of the desired software product. This chapter highlights the basic concepts about different specification languages such as, Z, B, Alloy, Monterey phoenix as well as the tools associated with these languages using an example of ATM system. The behavioral model of ATM system is mentioned in the fourth chapter. At the end of this chapter, an example of Cruise control system and a complex architectural style i.e., C2 (Component and Connector) is also explained.
2.2 Formal Modeling Language Z
The Z notation (ISO/IEC 13568 2002) is a formal specification language that offers mathematical notations for the specification process [3]. It provides precise semantics that remove ambiguities from specifications and offers a po-
tential for reasoning and automation. Z is an example of a state-based spec- ification language. Z Language has been developed at Oxford University by members of the Programming Research Group (PRG) within the Computing Laboratory. Z is a typed language based on first order predicate logic and set theory. Z is popular especially in developing critical systems where the reduc- tion of errors and quality of software is extremely important. It has undergone international standardization under ISO/IEC JTC1/SC22.
2.2.1 Z Notation
The main building blocks of Z notation are basic types definition, axiomatic definition, andschema definition. Figure 2.1 shows the basic type definition for an ATM system. A basic type definition introduces one or more types which are used to declare different variables used in Z specification. An example of basic type definition is the introduction of CARD with many types such as cardNo, acctNo, valid etc. An axiomatic definition is being used to describe one or more global variables, and it optionally specifies a constraint on their values. Figure 2.2 shows the axiomatic definition for an ATM system having both declaration part as well as predicate part. The condition in the predicate part should be satisfied throughout the specification.
CARD ::= cardNo|acctNo |issuingBank |valid NAME ::=custName |bankName
ATMResponse ::= opSuccess |opFailed STATUS ::= available |busy |idle RECEIPT ::=receipt
Figure 2.1: Basic type definition using Z notation
In order to model an operation of any system, schema is being used in the Z notation. A Z schema consists of a declaration and an optional list of
predicates. Figure 2.3 presents Bank schema and ATM schema having only declaration part.
minAmount :N maxAmount :N withdrawAmount :N accountBalance :N
withdrawAmount ≤maxAmount
Figure 2.2: Axiomatic definition using Z notation
Bank
bankName :NAME card :CARD
has :NAME →CARD balance :N
todayDate :DATE
ATM balance :N maxAmount :N todayDate :DATE
Figure 2.3: Schema definition using Z notation
2.2.2 Tools Support for Z Language
Various tools for formatting, type-checking and aiding proofs in Z are available.
CADiZ [26] is a UNIX-based suite of tools for checking and typesetting Z specifications. Z Type Checker (ZTC) [27] and fuzz tool [28] also support Z notation and type checking of Z specification. There is another tool named Z/EVES [12]. Z/EVES is an interactive tool for checking and analyzing Z specifications. Z/EVES is also able to read entire files of specifications that have been previously prepared using LATEX markup. RoZ [29] (Pronounce
asRosette) automatically generates the Z schemas skeletons corresponding to a UML class diagram.
2.3 Formal Modeling Language B
B was developed by Jean-Raymond Abrial, also took part in the creation of the Z notation during the 1980s [4]. B notation is closely related to formal methods Z and Vienna Development Method (VDM). B method has a strong decomposition mechanism. The primary aim of decomposition in B is to obtain a decomposition of proof. Formal verification of proof obligations ensures that a specification is consistent throughout its refinements [30]. Like Z and Alloy, B method is also based on first order predicate logic and set theory. The basic building block of B language is the notion of an abstract machine. An abstract machine is the specification of a B module, suitable for the construction of state variables and values of which must always satisfy its invariant.
2.3.1 B Notation
An abstract machine is a component that defines different clauses such as, data in the form of sets and constants, its properties, initializations and oper- ations. Figure 2.4 shows the different clauses such as, SETS, CONSTANTS, PROPERTIES, VARIABLES, INVARIANT, INITIALIZATION, and OPER- ATIONS specified in an order of the example as Bank ATM. But the order of these clauses is not fixed. The clause SETS represents the list of deferred sets used in the machine (ATM). CONSTANTS describe the type and properties of formal scalar parameters. PROPERTIES clause shows the type and properties of machine constants. VARIABLES represent a list of abstract and concrete variables used in machine. INVARIANT also describes the type and proper- ties of variables. INITIALIZATION clause is used to initialize the variables.
OPERATIONS clause list and define some specific operations. In this clause
entercard and enterpin operations are specified using mathematical logic.
MACHINE ATM SETS
ATMSTATE ={atmWaitCard,atmWaitPin,atmWaitOption}; CONSTANTS
minWithdrawal,maxWithdrawal PROPERTIES
minWithdrawal :INT&maxWithdrawal :INT VARIABLES
atmstate,atmcard INVARIANT
balance :INT&atmstate :ATMSTATE INITIALIZATION
balance :=minWithdrawal ||atmstate :=atmWaitCard OPERATIONS
entercard = PRE atmstate =atmWaitCard
THEN IF atmcard =valid THEN atmstate :=atmWaitPin ELSE atmstate :=atmErrorMSG END END;
enterpin = PRE atmstate =atmWaitPin
THEN atmstate :=atmWaitOption END;
Figure 2.4: Abstract state machine representation using B notation
2.3.2 Tools Support for B Language
Two main commercial tools which support B language i.e., Atelier B [13] and B-Toolkit [31] are used by researchers and developers. For method B, there is a model checker tool, known as ProB [32], developed at the University
of Southampton. The model checker ProB, includes an animator, which is amenable to validate the simulated behavior of a specification. UML-B [30] is a tool that translates UML class diagram and UML statechart diagram into B notation. But this tool work under certain conditions. Atelier B proposes a set of commands allowing [13]:
• Syntax and type checking of components.
• Automatic generation of proof obligation.
• Automatic demonstration of proof obligations.
• Translatable language checking.
• Translating into one of the following programming languages (C, C++, ADA, HIA).
2.4 Formal Modeling Language Alloy
Alloy is a lightweight formal method for describing structural properties of a system. Some researchers believe that the formal methods are emphasized on full formalization of a specification or design [33]. According to them, com- plete formalization of a complex system is a difficult and expensive task. But nowadays, various lightweight formal methods, which emphasize partial spec- ification and focused application, have been proposed. Alloy is an example of this lightweight approach. Alloy offers declaration syntax compatible with graphical object models, and a set-based formula syntax powerful enough to express complex constraints. There are many other powerful formal methods also available such as, Z, B, VDM, CSP, RSL, etc., but they are generally not directly executable. Alloy is amenable to a fully automatic semantic analysis that can provide checking of consequences, consistency, and simulated exe- cution. Alloy specification is built from atoms and relations. An atom is a primitive entity that is indivisible, immutable, and uninterpreted [34]. The semantics of Alloy bridges the gap between Z and object models. Alloy is
mainly designed to search for instances within finite scope. The main building blocks of Alloy modeling language are: signature, field, predicate, function, fact, assertion, command and scope. A signature is a collection of fields. A field represents a relation between atoms. The signature can be represented by a keyword sig.
2.4.1 Alloy Notation
Figure 2.5 shows the Alloy specification of ATM system having a module ATM to split a model among several modules. A module in Alloy allows constraints to be reused in different contexts. This specification has two abstract signa- tures such as, ATM STATE and OPERATION. Abstract signature can not generate instances. A signature ATM contains some fields for showing relations with other signatures. These fields are associated with multiplicity keywords such as, lone, one for representing different types of relationships.
module ATM
abstract sig ATM STATE{}
abstract sig OPERATION{}
sigATM{ pin : loneIdentifier, card : loneIdentifier, state : oneATM STATE,
balance : Identifier−> one Int, operation : OPERATION }
pred enterCard[atm, atm′ : ATM, cId : Identifier]{ atm.state = ATMWaitCard && atm′.card = cId &&
atm′.balance = atm.balance && atm′.state = ATMWaitPin }
Figure 2.5: Alloy notation for ATM system
In Alloy, operations are specified using predicates. A predicate is a logical
formula with declaration parameters. In Figure 2.5, enterCard operation is specified using pre-state and post-state of ATM. In this specification,atm and atm’ are instances of ATM showing a state of ATM, beforeenterCard operation and after enterCard operation respectively.
2.4.2 Tools Support for Alloy Language
Several research works have been carried out to the integration of semi-formal specification languages (like UML) with formal specification Languages. UML- 2Alloy [35] is a tool for integrating UML and Alloy into a single tool. Using UML2Alloy, the designer can take advantage of the positive aspects of each modeling language. Alloy supports an automated tool called, Alloy Analyzer [16] which analyzes the Alloy models.
Formal models written in Alloy language, are translated into satisfiabil- ity problem using SAT solver [36]. After that SAT solvers are invoked to exhaustively search for satisfying models or counterexamples. In Alloy, addi- tional constraints can be added as assertion and they can be verified about its satisfiability. If an assertion does not satisfy the Analyzer, it produces a coun- terexample in the form of instances. In order to generate instances for given specification, a predicate is used. If there is a requirement of any additional constraints, those can be added using fact and assert keywords.
2.5 Modeling Language Monterey Phoenix
Monterey Phoenix (MP) helps to describe the structure of possible event traces using event grammar rules and other logical constraints [37]. Schemas are in- stances of behavior. Schema formalizes the software architecture on the basis of behavioral models. The system is defined as a set of events also known as event trace, with two basic relations such as precedence and inclusion [38]. Event trace is formally specified using event grammars and other logical constraints
organized into schemas. Phoenix Schema is based on the concept of event (ac- tion) including time constraint and introduces an ordering relation for events.
In a system execution, two events may not be necessarily ordered. They may even execute simultaneously. For Phoenix Schema, both relations (inclusion and precedence) satisfy non-reflexivity, transitivity, and non-communicative properties. Ten number of axioms [37] may be used for ordering of events that should hold for event traces.
1. P :: Q R; denotes event traces. 4. P :: [Q]; denotes an optional event Q.
P P P
or
Q R Q 2. P :: (Q | R) ; denotes an alternative events (Q or R).
P P 5. P :: {Q, R}; denotes set of events Q Or and R without an ordering.
Q R P
3. P :: (* Q *) ; denotes zero or more events (Q). Q R
P 6. P :: {* Q *} ; denotes zero or more events (Q) without an ordering.
P Q Q Q
Q Q Q
Figure 2.6: Rules of ordering of events using IN and PRECEDES
Events are represented by small circles and arrows using two relations such as inclusion (IN) and precedence (PRECEDES):
IN −→
PRECEDES =⇒
2.5.1 Event Grammar Rules for Monterey Phoenix
For ordering of events, let us assume that there are three events i.e., P, Q, and R. The rule P :: Q R; means that an event p of type P contains ordered events q and r of types Q and R (q IN p, r IN p, and q PRECEDES r).
Figure 2.6 shows the rule of ordering of events using two relations (IN and PRECEDES). For phoenix schema, tool is not ready by the developers for industrial application. Auguston et al. [39] have proposed a model checker for monetary phoenix based on PAT [17] verification framework.
2.6 Cruise Control System (CCS)
The CCS is an automatic electronic control system used in a car to assist the driver for an automatic transmission [40]. Cruise controller is the main compo- nent of CCS that provides automated control over the vehicle by maintaining constant vehicle speed with the help of input from the driver and communica- tion with other vehicles. UML class diagram of CCS is shown in Figure 2.7.
This diagram contains nine classes i.e., AxleSensor, EngineSensor, BrakeSen- sor, GPS, WheelRevSensor, Clock, CruiseController, ThrottleActuator, and GUI. In CCS, axle sensor is being connected to the axle that generates a fixed number of pulses per rotation of the axle. Engine sensor is being connected to the engine generates signals when the engine is in on state and off state respectively. Brake sensor connected to the pedal sends a signal when the pedal is pressed or released. Global positioning system (GPS) is a navigation satellite system that can provide speed and location of the vehicle. Wheel revolution sensor generates signals when speed of the vehicle gets changed. All sensor classes have its states at any particular time. On receiving clock’s signal- notification from the classClock, the states of these sensor classes gets changed.
After changing their states, sensor classes send notification toCruiseController class.
Figure 2.7: Class diagram of Cruise Control System
Cruise controller is the main class of CCS that allows the driver of the vehi- cle to maintain speed without pressing the accelerator pedal. Cruise controller sets the desired speed to the currently measured speed and then attempts to maintain the measured speed. When accelerator is pressed and the cruise con- troller is on, the vehicle accelerates smoothly. Cruise controller can change the position of the throttle. If the driver pushes the brake, the cruise controller switches off immediately. There are two actuators, which are considered in this class diagram such as, ThrottleActuator and GUI. Cruise controller pro- vides the states of sensor classes to actuators on the basis of requirements.
GUI class is helpful for the driver to see navigation, fuel level, and speed of the vehicle. For more detail about behavior of Cruise control system, C2 style architecture is presented in chapter 5.
2.7 Architectural Style C2
The goal of this thesis is formalization of architectural styles. Large number of architectural styles are available in literature such as, client-server, virtual- machine, object-oriented, pipe and filter etc. but these styles are not useful for all types of application systems. In chapter 4, ATM system is designed using object oriented style (class diagram), subsequently formalized using dif- ferent formal methods. For complex heterogeneous system like Cruise control system, simple architectural styles are not sufficient. Hence, some complex architectural styles are felt to be more helpful to explain the behavior of any complex application systems. Accordingly it is observed that Component and Connector (C2) style is suitable for these types of complex systems.
C2 is a message-based architectural style for developing flexible and exten- sible software system. It is based on layers of concurrent components linked by connectors in accordance with a set of rules [41]. Communication among components is done by implicit invocation. The principle of C2 style is to pro- vide limited visibility among components. A component in a C2 style is only aware of services provided by other components above it in the hierarchy. A component is completely unaware of services provided by components beneath it. In a C2 style, a component placed at the bottom layer utilizes the services of components above it by sending a request message. Components at the upper layer emits the notification messages, when they change their states. C2 connectors broadcast notification messages to every component and connector placed at the bottom layer. Thus, notification messages are represented as implicit invocation mechanisms, which enable several components to react to a single component’s state change [42].
Figure 2.8 shows the example of C2 style developed in a tool known as, AcmeStudio. An architectural interchange language models an architectural style by using AcmeStudio. This tool does not support C2 style. An event-
S T S E U Q E R
N O T I F I C A T I O N S
Figure 2.8: An example of C2 style
based style is shown in Figure 2.8; as C2-style is much similar to an event-based style. In this figure, there are seven components, two C2 connectors, and nine links. Component6 and component7 send only request messages to upper layer components, whereas component1, component2, and component3 broadcast only notification messages to the lower layer components. Component4 and component5 send request messages and broadcast notifications to upper layer components and lower layer components respectively. A software architecture has four main elements such as component, connector, port, and role. These elements are described below:
Component : A software component is an architectural element that encapsulates processing and data in a system’s architecture. It restricts access to a subset of the system’s functionality and/or data via an explicitly defined interface. It can be deployed independently [43]. A software component has a set of runtime interfaces, known as a port. The port allows the points of interactions between the component and connector.
Connector : In a complex and distributed heterogeneous environment, interaction may become more important and challenging than the functionality of the individual components. A software connector has the task of effecting and regulating interactions among components. It also provides application- independent interaction facilities. A connector has a set of roles that identifies the components and connectors in the interaction.
Port : It is not possible in current component models to deal separately with an element of an interaction point when such an element is needed alone for specifying a specific logic [44]. A port defines the points of interaction of a component with its environment. Components with complex interfaces are overloaded with many different ports.
Role : In software architecture, components cannot directly connect to connectors. They require a suitable role in connector that are compatible with a port in the component. A role helps to facilitate the interaction between a connector and a component. A connector is composed of roles that are connected to specific ports. The roles are used to specify interfaces of the port, being used.
2.8 Conclusion
In this chapter, important notations associated with different formal modeling languages, a safety critical system, and a particular software architectural style have been presented. For automatic verification process, a number of tools are available in literature. The goal of this chapter is to provide fundamental information about techniques and tools for the research work carried out.
Literature Survey
3.1 Introduction
Effort given for software testing can be reduced by applying formal verifica- tion techniques from starting phase of software development process. There are many formal specification languages available for the formalization of soft- ware. The state-of-art of various techniques applied for formalization and model checking of real-time systems and different architectural styles are men- tioned in the following sections.
3.2 Formalization of Behavioral Models
The first proposed work is a formalization of a behavioral model using state- based and event-based approaches using a case study i.e., ATM system. It is a comparative study, in order to assess the strength and weakness of different for- mal methods. A number of literatures available in the area of formalization of behavioral model and comparison among different formal modeling techniques.
Nami and Hassani [45] described properties and types of formal specifica-
tion languages such as, Z language, VDM, RSL and CSP in software engineer- ing. They categorized modeling languages into model-oriented, constructive, algebraic, process-model, hybrid, and logical. They addressed the benefits and barriers of these modeling languages. They did not describe about tool sup- port for these specification languages. They categorized these specification languages on the basis of associated properties.
Yusuf and Yusuf [46] have compared the properties of five formal methods i.e., Z language, UML, The B method, Petri Nets, and Action Systems. They addressed their differences by designing a particular part of the Automated Banking Machine (ABM) using each method, and further compared these methods by analyzing their strengths and weaknesses. For syntax checking and theorem proving, generally tools are used but they did present verification process.
Daniel Jackson [47] introduced a comparison of notations among Z, UML, and Alloy. He compared the notations used in three modeling languages using an example of family. According to his conclusion, Z and Alloy are formal approaches whereas, UML is a semi-formal technique. UML is a graphical approach whereas, Z and Alloy are textual languages. The notations of Alloy are inspired from Z and UML. They did not address the tools associated with these modeling languages.
Zhang et al. [39] developed an approach for modeling and verifying software architectures using an event-based approach i.e., Monterey Phoenix (MP).
Firstly, they formalized the syntax and operational semantics using MP. Sec- ondly, a dedicated model checker for MP is developed based on the PAT verification framework. They modeled software architecture using Monterey Phoenix but automatic verification process did not show. They have proposed a tool for Monterey Phoenix but this tool is not ready for industrial application.
Habrias and Frappier [48] compare various techniques such as UML, Z, TLA+, SAZ, B, OMT, VHDL, Estelle, SDL and LOTOS etc. They compared
these formal methods related to a set of attributes, which described several properties of specification methods. In their study evaluation parameter is not properly defined.
Kumar and Goel [49] modeled some aspects of ATM system using Z no- tation. Firstly, they described the conceptual and formal models of the ATM system. For writing the Z schemas and other notations, they have used the Z Word tool. There are many theorem provers such as Z/EVES, HOL-Z, Proof- Power etc. available for specification language Z. But authors have used Z Word tool that provides only syntax checking of the Z specification written in Microsoft Word.
3.3 Model Checking of Software Architectural Styles
Software architecture is helpful for the high level design of a system in terms of components and connectors. The main building block of software architecture is an architectural style that provides domain specific design semantics for a particular system. Although many architectural description languages (ADLs) are available in the literature for modeling notations to support architecture based development. These ADLs lack proper tool support in terms of formal modeling and visualization. Hence, formal methods are used for modeling and verification of architectural styles. Lots of work has been done in formalization and model checking of simple architectural styles using different architectural description languages (ADLs) as well as formal modeling languages. Some of them are discussed in this section.
Kim and Garlan [50] have mentioned about mapping of an architectural style into a relational model. They expressed an architectural style using formal modeling language Alloy which can be used for checking properties
such as:
• Whether a style is consistent
• Whether a style satisfies some logical constraints over the architectural structure
• Whether two styles are compatible for composition
• Whether one style refines another or not
They have proposed formal modeling techniques for simple architectural styles such as client-server, pipe and filter, virtual machine etc.
Wong et al. [51] presented a technique to support the design and verification of software architectural models using the model checker Alloy Analyzer. They presented the use of the architecture style library in modeling and verifying a complex system that utilizes multi-style structures. They have developed formal notations for simple architectural style i.e., client-server style using modeling language Alloy.
Heyman et al. [52] illustrated the need of formal modeling techniques for the software architect who need to precisely ascertain the security properties of their design models. They have proposed a technique that motivates an architect to easily develop, secured architecture designs by assembling already verified security pattern models. They have developed a formal model for simple security design pattern.
Keznikl et al. [53] presented an approach for Automated Resolution of Connector Architectures based on constraint Solving techniques (ARCAS).
They used a formal modeling language Alloy for describing a connector theory.
They employed a constraint solver to find a suitable connector architecture as a model of the theory. They exploited a propositional logic with relational calculus for defining a connector theory.
Bertolino et al. [54] illustrated software architecture-based analysis, eval- uation, and testing. In this paper authors reported those parameters that consider the most relevant advances in the field of architecture based test-
ing and analysis over the years. This study is a state of art described about analysis, evaluation, and testing processes.
Zhang et al. [55] described the formal syntax of the Wright architectural description language together with its operational semantics in the Labeled Transition System (LTS). They presented an architectural style library that embodied commonly used architectural patterns to facilitate the modeling pro- cess. They had considered the Teleservices and Remote Medical Care System (TRMCS), as a case study. They have modeled only simple architectural styles such as client-server, pipe-filter, publish-subscriber, and peer2peer by consid- ering TRMCS as a case study.
Pahl et al. [56] presented an ontological approach for architectural style modeling based on description logic as an abstract, meta-level modeling in- strument. They introduced ontologies as a mechanism described and formally defined architectural styles. They proposed a framework for style definition and style combination. They used ontologies as a mechanism for describing and formally defining architectural styles.
Hansen and Ingstrup [57] have presented an application of the Alloy mod- eling language to model architectural change. They demonstrated that it is possible to model architectural change in a relational, first-order language us- ing both a static and dynamic model of the architectural runtime structure and architectural runtime change respectively.
Bagheri et al. [58] described the feasibility of automated computation of architectural descriptions with an executable prototype developed in Alloy.
Firstly, they identified the behavior of architecture as an independent variable.
Subsequently a conceptual architecture considered to make this idea precise, including a graphical notation showing how the key concepts relate to each other has been explained. For modeling KWIC (key word in context), they have considered many simple architectural styles such as, pipe-filter, object- oriented, and implicit-invocation style.
3.4 Conclusion
This chapter makes a thorough survey of formalization and model checking of behavioral model and architectural styles. The emphasis is given mostly on the formalization of different architectural styles such as pipe-filter, client- server, publish-subscriber, peer2peer. Apart from these, many comparative approaches also mentioned in this chapter. However, it could be seen that for- malization of critical and complex systems is a challenging task. This provides a motivation for selecting an appropriate style for the available application and subsequently formalizing using suitable formal methods.
Formal Verification of Behavioral Model
4.1 Introduction
To specify requirements, formal methods are mathematical based techniques for the specification, verification and development of a system. It plays an important role for software developers in the analysis and design phase of the software development life cycle. In this chapter, formal model of Bank ATM [59] system using well known formal specification languages such as Z [3], B [4], Alloy [6], and Monterey Phoenix [37] have been developed. For verification of these models, tools such as, ”Z/EVES” [12], ”Atelier B” [13], and
”Alloy Analyzer” [16] [60] are used to verify the specifications of ATM system being developed using languages Z, B, and Alloy. Currently, for Monterey Phoenix, literature does not provide any tool. Alloy Analyzer helps to make a Phoenix Schema executable. Z, B, and Alloy are state based methods whereas, Monterey Phoenix is an event based approach. Z, B, and Alloy are used for sequential systems whereas, Monterey Phoenix is helpful for parallel systems.
Alloy and B are inspired by Z which is more expressive than both Alloy and B but it is intractable in nature. The stylized typography of Z makes it harder to work. ATM system is an example of real-time system and its incorrect functioning may lead to large scale economic imbalance.
To specify requirements using formal methods, an example of Automated Teller Machine (ATM) [59] is being considered, whose primary function is to withdraw cash, make an enquiry of balance, and transfer fund.
Figure 4.1: Statechart diagram of ATM system
The statechart diagram of the ATM system has been shown in Figure 4.1. Statechart diagram is used to model the dynamic behavior of a system.
It defines different states of an object during its lifetime. These states are changed by events. Statechart diagrams are useful to model reactive systems that respond to external or internal events. In Figure 4.1, the statechart
diagram has many states such as wait for PIN, wait for an operation, processing withdraw etc. as well as many events such as insert card, enter PIN, select withdrawal etc. When any event occurs in any state then that state will change to some other state.
4.2 Formal Specification using Z
Z specification of ATM system is based on the finite state machine (FSM) representation. In Z specification, the main building blocks are basic type definition, axiomatic definition, and schema notation. To formalize an ATM system, it first declares the main variables that are used in Z schema, such as debit card related information, type of ATM response, date, and messages in the form of output generated by ATM system. Basic type definition for the ATM system is described in Figure 4.2.
[ATM,CUSTOMER,Bank]
CARD ::= cardNo|acctNo |issuingBank |valid ATMResponse ::= opSuccess |opFailed
STATUS ::= available |busy
DATE ::=issueDate |expiryDate |todayDate
ERRORMessage ::=invalidePinNo |invalideCard |insufficientBalance Figure 4.2: Basic type definition of ATM using Z
For withdraw cash operation, the customer should be aware in advance about different restrictions for withdrawal. Different banks provide certain restrictions on minimum amount or maximum amount of withdrawal. Hence, it needs to be specified. The axiomatic definitions of some important constraints are given in Figure 4.3.
minAmount :N; maxAmount :N
withdrawAmount :N; moneyInMachine :N accountBalance :N; pinNo :N; maxTran :N withdrawAmount ≤maxAmount
Figure 4.3: Axiomatic definition of ATM using Z CardReader
card? :CARD; date :DATE
status :STATUS; message! :ERRORMessage status =busy
date =expiryDate ⇒message! =invalideCard
Figure 4.4: CardReader schema using Z
Z schema has two parts i.e., declaration part and predicate part. The Z schema CardReader has both declaration as well as predicate part that is shown in Figure 4.4. The first variable in the declaration part of the schema CardReader is acard?, which represents input variable and the second variable ismessage! which represents an output variable. In Z, the input variables are represented by using “ ? ” symbol and the output variable is represented by using “ ’ ” symbol.
BalanceEnquiry and CashWithdraw schemas are represented in Figure 4.5 and Figure 4.6 respectively. In BalanceEnqury schema, ΞATM and ΞBank denote that the state of schemas of ATM and Bank will not change after completing BalanceEnqury operation. The variable moneyInMachine’ and accountBalance’ represent the next state of variables moneyInMachine and accountBalance by using “ ’ ” operator. In schema CashWithdraw, ∆ATM and ∆Bank represent that after the withdrawal operation the state of ATM
and the state of Bank both will change. Z schemas can be specified using other schemas with the Ξ and ∆ symbols when specifying operations that respectively change the state or leave the state unchanged. The operator ⊕ is used for override operation. Override operator is used in CashWithdraw schema in order to override the remaining balance in previous balance after withdrawal operation.
BalanceEnquiry ΞATM
ΞBank
response! :ATMResponse accountBalance :N receipt! :RECEIPT status :STATUS status =busy
moneyInMachine′ =moneyInMachine accountBalance′ =accountBalance response! =opSuccess
receipt!.amount =accountBalance status′ =idle
Figure 4.5: BalanceEnquiry schema using Z
For syntax checking and theorem proving of Z specification, Z/EVES tool has been considered. The whole declaration part checked by Z/EVES tool with the help of type definition of specification. The whole predicate part proved by using Z/EVES tool with the help of specified constraints. The output generated by the Z/EVES tool is presented in Figure 4.7.
CashWithdraw
∆ATM
∆Bank
acct? :ACCOUNT; m? :N balance :N
response! :ATMResponse receipt! :RECEIPT status :STATUS status =busy
balance′ =balance⊕ {(acct? 7→balance(acct)−m?} response! =opSuccess
receipt!.amount =m? satus′ =Idle
Figure 4.6: CashWithdraw schema using Z
Figure 4.7: Syntax and type checking using Z/EVES tool
4.3 Formal Specification using B
B method is a complete formal method, which supports a large segment of the software development life cycle such as specification, refinement, and im- plementation. B ensures refinement steps and proofs, that the code satisfies its specification. The main building block of B specification is an abstract machine which is used to encapsulate state variables, initialization of these variables, and values of which always satisfy its invariant (predicate). The be- havioral aspect of this specification is specified in terms of initializations and operations that may be used to access or modify this abstract state. In this study, important states and operations of Bank ATM system using B notation are specified and further refined.
ATM has been considered as a state machine having two sets namelyATM- STATE andCARDSTATUS, and four constants that are represented in B spec- ification of ATM. Also two types of variables, namely, ABSTRACT VARI- ABLES and CONCRETE VARIABLES are considered to store the values.
It is required to specify invariants and initialize ABSTRACT VARIABLES and CONCRETE VARIABLES. The first operation is considered as enter- card. The initial state of this operation isatmWaitCARD. If the card is valid then ATM system requests for PIN (Personal Identification Number), other- wise it displays an error message as atmErrorMSG. After verification of PIN, ATM system displays set of options for different operations. In Figure 4.8, the operations such as balanceEnquiry, withdrawCash, and transferFund are specified in an abstract way. Further in the refinement process, other states may be specified.
In Figure 4.8, the important properties of ATM system are represented in an abstract view. Now it has been refined as withdrawCash operation and transferFund operation. In the refinement process, some more variables and invariants are considered those are shown in Figure 4.9. Two abstract variables
