Một khung làm việc kiểm chứng cho quy trình phát triển phần mềm lấy đặc tả làm trung tâm

Nội dung text: Một khung làm việc kiểm chứng cho quy trình phát triển phần mềm lấy đặc tả làm trung tâm

1. Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 19 5(48) (2021) 19-30 A verification framework for specification centered developments Một khung làm việc kiểm chứng cho quy trỡnh phỏt triển phần mềm lấy đặc tả làm trung tõm Vũ Diệu Hương* Vu Dieu Huong* Information Technology Department, Economic Information System and E-Commerce Faculty, Thuong Mai University, 79 Ho Tung Mau, Hanoi, Vietnam Văn phũng Cụng nghệ Thụng tin, Khoa Thương mại Điền tử và hệ thống Thụng tin Kinh tế, Trường Đại học Thương mại, 79 Hồ Tựng Mậu, Hà Nội, Việt Nam (Ngày nhận bài: 18/6/2021, ngày phản biện xong: 19/8/2021, ngày chấp nhận đăng: 17/10/2021) Abstract Requirement specifications are initial inputs of every software development process. Referring to the specification is frequently needed through the software development phases. Because the specification has such a tremendously important role in the software process, its quality should be ensured before it is used to drive life – cycle activities. Once the quality of the specification is ensured, it is reliable input to verify the other artifacts outputted from various development activities like design and implementation. In this paper, we propose a verification framework for specification centered developments. In this framework, we firstly focus on improve the quality of specification then use such high-quality specification to drive the verification of the design and the implementation. This framework could be applied in domain of reactive systems with high automation, adaptation, and practicality. Keywords: software verification; formal verification; specification centered development; reactive systems. Túm tắt Đặc tả yờu cầu là đầu vào khởi đầu của mọi tiến trỡnh phỏt triển phần mềm. Tham chiếu tới đặc tả là cần thiết ở mọi pha trong tiến trỡnh phỏt triển phần mềm. Vỡ đặc tả cú vai trũ đặc biệt quan trọng như vậy, chất lượng của đặc tả nờn được đảm bảo trước khi nú được sử dụng để dẫn xuất mọi hoạt động của vũng đời phỏt triển phần mềm. Một khi chất lượng của đặc tả đó được đảm bảo, nú sẽ là một đầu vào tin cậy để kiểm chứng cỏc chế tỏc được cung cấp bởi cỏc hoat động khỏc nhau trong vũng đời phỏt triển phần mềm, vớ dụ như mụ hỡnh thiết kế, chương trỡnh. Trong bài bỏo này, chỳng tụi đề xuất một khung làm việc kiểm chứng cho tiến trỡnh phỏt triển phần mềm lấy đặc tả làm trung tõm. Trong khung làm việc này, đầu tiờn chỳng ta sẽ tập trung vào cải tiến chất lượng của đặc tả rồi sử dụng đặc tả cú chất lượng được đảm bảo này để dẫn xuất cho hoạt động kiểm chứng thiết kế và chương trỡnh. Khung làm việc này cú thể được ỏp dụng trong miền cỏc hệ thống phản ứng với tớnh tự động húa cao, tớnh thớch nghi tốt và tớnh thực hành cao. Từ khúa: kiểm chứng phần mềm; kiểm chứng hỡnh thức; phỏt triển phần mềm lấy đặc tả làm trung tõm; cỏc hệ thống phản ứng. *Corresponding Author: Vu Dieu Huong; Information Technology Department, Economic Information System and E- Commerce Faculty, Thuong Mai University, 79 Ho Tung Mau, Hanoi, Vietnam Email: huongvd@tmu.edu.vn, vudhuong@gmail.com
2. 20 Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 1. Introduction highly destructive effects on the human life and Requirement Specifications [15] the assets. (Specifications for short) describe expected Quality improvement for RS in a unified (external) behaviors of the software. They also verification process is still a great challenge. describe nonfunctional requirements, design What we need for such verification process constraints and other factors necessary to includes: (i) a high-quality specification which provide a complete and comprehensive is consistent and validated against user description of the requirements for the requirements; (ii) this specification is used as a software. confident input to formally verify both of the Specifications are initial inputs of every design and the implementation. We know that software development process. Moreover, they there exists a gap between the specification and are involved in every phase of the development the design. The specification defines abstract processes. Referring to the specification is data structures, whereas the design defines frequently needed through the software implementable data structure. Also, the development phases. In other words, various specification defines results of operations, development activities are based on while the design defines details of how to make specifications: design, implementation, testing, the results. There are two main approaches for maintaining. Specifications are used as the verification of every software including basis for providing and ensuring the quality of reactive systems. In the first approach, we can designs and implementations. describe the specification in an appropriate specification language like Z [7], VDM Because the specification has such a (Vienna Development Method) [6], Event-B tremendously important role in the software [5]; then, we derive the behaviors of the design process, its quality should be ensured before it from the higher-level specification as adopted is used to drive life – cycle activities. Once the in [5]. The problem of this approach is that in quality of the specification is ensured, it is order to represent highly optimized behaviors reliable input to verify the other artifacts of reactive systems, we need to use various outputted from various development activities complex data structures and control structures. like design and implementation. Therefore, directly deriving these behaviors Reactive system [16] (RS for short) is a from the abstract specification is generally very system that continuously interact with its hard. In the second approach, we can use environment by responding to external stimuli. imperative specification languages like Promela For example, vending machines, elevator, and [8] to describe the design. This facilitates operating systems are reactive systems. The describing the highly optimized behavior by environment of a vending machine includes using various data structures and control customers who want to buy products restocked structures. In this approach, the specification or in that vending machine; and, the environment the properties we want to check can be of an operating system includes software described in temporal logic. However, we applications running on that operating system. consider that temporal logic formulae, which Several reactive systems are considered as allows us to describe properties about safety-critical (e.g., operating systems for invariants on some variables and the relative mobile vehicles). Such kind of systems should order of event calls, but are not adequate for be seriously verified because their errors cause describing the important properties of reactive
3. Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 21 system concern with the pre-condition and the specification and the design to facilitate the post-condition of each event invoked from their description of them. That is, Event-B is adopted environment. Moreover, we could not ensure for the specification and Promela for the the consistency of these properties in the design. We deal with the difference between temporal logic formulae. Also, such formulae specification languages for the specification are not appropriate inputs for verification of the and the design by common semantics, label implementation. transition systems (LTSs), and correspondences Our idea is using the rich notions (e.g. sets between state transitions given by mappings and relations) in the formal specification from syntactic elements in the former to those languages like Event-B, we could easily in the latter. This approach is also applied to describe properties we want to verify. deal with the gap between the specification and Therefore, we intendedly use Event-B to the implementation. Therefore, our framework facilitate describing properties of the reactive accepts any programming language used in the system. In Event-B, one can describe the implementation. In other words, the system as a set of events and the behavior of specification described in Event-B is also each event can be specified as pre-conditions appropriate input to verify the implementation. and post-conditions using the rich notions. It This makes it possible to systematically ensure also provides a facility to verify the consistency the quality of reactive systems based on the and the correctness of the properties. This confident specification with high automation, results high-quality specifications. Furthermore, adaptation, and practicality. such specifications are appropriate inputs to 2. Related works automated verify the implementation. Using formal specifications as inputs for For verification of the design, our idea is to software verification is presented in [1] and describe the design in imperative specification [14]. [1] presents an approach to verify the OS languages like Promela, which is easy to kernel by applying theorem proving. Theorem represent the design. We think that dealing with proving can be used to verify the infinite the specification and the design based on the systems; but, it generally requires a lot of different specification languages is appropriate interactive proofs. [14] applied the model for systems in which there exists a big gap checking technique to verify the correctness between the specification and the design like properties of safety and liveness of target the reactive systems. Then, we verify the design systems. In our workflow, we use model against the specification. In this case, we must checking combing with prover tools of Event- deal with the difference between the language B. Although ranges are bounded due to the used to describe the specification and that for limitation of model checking; however, we are the design. able to improve quality of the properties In this paper, we propose a verification checked and get completely automatic framework for Specification Centered verification. Therefore, we have a high degree Developments in which Specifications are of confidence in the verification results. verified first; Specifications are used as the Animating Event-B models is implemented in inputs for ensuring the quality of designs and ProB [2] and Eboc [3]. In these approaches, the implementations. In our framework, we intend target models are described in Event-B. ProB to use different specification languages for the and Eboc directly check the target models
4. 22 Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 against the internal consistency. We use Rodin Three verification activities are shown in the prover of Event-B to ensure the internal Fig.1. The first activity is formalizing and consistency and use our animator to validate. validating the requirements. This step provides We use our own tool to generate the LTS of the the high-quality formal specification of Event-B specification. Formal Specification requirements. The second activity is checking Centered Development Process is presented in the design against the formal specification. [4]. However, this work applies model This step uses the formal specification as a checking technique to give test suite from the reliable input to verify the design by applying formal specification. Our framework uses the model checking technique [8]. The last activity formal specification for not only verification of is checking the implementation against the the design but also that of the implementation. formal specification. Also, this step uses the 3. Verification framework formal specification as a reliable input to verify the implementation by applying testing Our framework is illustrated in Fig.1. Initial technique [13]. As mentioned earlier, this input of the framework is a statement of user framework adapts to overall software requirements. That is an informal description of development processes such water fall, user requirements. Originally, the user evolution model, agile methods. The requirements are usually described in natural verification is an ongoing process and the languages. Due to the ambiguity of natural verification activities are integrated in the languages, such informal descriptions could development activities. Once, both of the lack consistency. Moreover, they are not proper design and the implementation conform to the inputs for the formal verification. Therefore, we specification, we are confident that the need formal specifications replacing for the implementation also conforms to the design. informal ones to drive life - cycle activities Actually, we could show the conformance including verification of the designs and the between the implementation and the design by implementations. The quality of formal applying the same approach. specifications should be ensured before we use them to drive life - cycle activities. 4. Formalizing and validating requirements in Event-B 4.1. Requirements of reactive systems Features or aspects of reactive systems are commonly mentioned as (i) external behavior or functional requirements, (ii) properties or non-functional requirements, (iii) communication or links between controllers and physical entities like sensors and actuator [9], and (iv) communication between reactive systems and their environments [10]. Our framework focuses on verifying quality of Specification, Design and Implementation for reactive system. This section aims at how to Fig.1: Verification Framework (steps) provide a high-quality specification. In our point of view, a high-quality specification is
5. Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 23 one that (1) it has sufficient requirements for (events) on the variables, and state invariants. user’s needs and (2) it is well structured, The variables are typed using set theoretic unambiguous, consistent, readable, and easy to constructs such as sets, relations, and functions. review and validate. The events are defined with their guard The requirements are generally divided into conditions and substitutions (so-called before functional requirements and non-functional and after predicates), which allow both requirements (i.e. constraints). In the deterministic and non-deterministic state specification of reactive systems, we focus on transitions. the behavioral aspect of target systems in Event-B is appropriate to describe communication with their environments. Such requirements of reactive systems. Services are aspect concerns with system services and specified in terms of events with high-level constraints on service operation in operational definition of state changes by combination with the environment. For guarded substitutions. An event is made of two example, services of Vending Machine (VM) elements: (1) a guard that states the necessary include switch on, switch off, restock an item conditions for the event to occur, and (2) a into VM, collect coins, and dispense an item to substitution that defines the state transition the customers. A few of constraints on these associated with the event. The semantics of the services are as below: events define the overall results of the Pushing a button shall vend an item of the executions; therefore, represent pre-conditions type corresponding to that button and post-conditions of the services. The machine shall retain exactly item cost The Rodin tool supports not only describing for each item vended but also verifying Event-B models. In The machine shall return all deposited particular, it has a capable of checking the money in excess of item cost internal consistency. This capability is provided The machine shall flash the light for a by Proof Obligation Animator and Prover [5], selected item while vending is in progress to which are included in the Rodin tool. The indicate acceptance of a selection to the animator generates verification conditions as buyer. proof obligations. By discharging such Constraints are divided into two kinds of verification conditions, we could show the conditions. The first one is pre-condition, that consistency of the specification. is, the condition under which a service is Fig. 2 demonstrates a specification of the activated. Another one is post-condition, that is vending machine in Event-B. Variable itemList action or result of service execution. For defines a set of items that are currently example, when the customer inserts a coin, available to be dispensed. It has an abstract data collected coins must activated and the credit is type namely ITEMS. The variable numCup increased by the value of coins. holds the number of cups in the itemList. Its type is an arbitrary set of non-negative integer. 4.2. Formalizing requirements using Event-B The variable amount defines the total of money Formal specification described in Event-B is deposited so far and available to make a regarded as a highly abstracted level purchase. Its type is an arbitrary set of non- description of the systems. This description negative float. mainly consists of state variables, operations
6. 24 Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 External behaviors are specified in terms of events in Event-B namely switch-on, switch- off, insert, restock, and dispense. Set operations (e.g. union, set minus) are used to describe what the system behaves when an item is restocked or dispensed. A mechanism to add an item into set avail and remove the corresponding item from the set has not been described. Also, the specification describes what happens when the customers insert cash or credit; however, how to recognize them and compute the total deposited money is postponed to describing the design. The specification could be also described in any model-based languages VDM or Z because they also provide rich notions like set, relation, and function. In this paper, we adopt Event-B because Event-B models are event-driven Fig.2: Specification of Vending Machine models, which are close to reactive systems. Communication between the animator and 4.3. Validating formal requirements the users is described in the following steps: We develop an animator for Event-B 1. Starting at the initialization, the animator specification to give a visualization of the enumerates all possible values for the specified system’s behavior. This assists the constants and variables of the specification analyzers, users and stake-holders to validate that satisfy the initialization and the formal specifications against informal invariant to compute the set of initial states. requirements by demonstration of state 2. The animator prompts the users to enter a transitions and stimulus – response behaviors of stimulus the target systems in the combination with their 3. The animator finds all possible values for environments. While animating the specified event parameters of an individual event to system’s behavior, the users give stimulus as evaluate the guard of that event. If the guard they are the target system’s environment. holds in the given state, the animator computes the effect of the event based on substitution of that event. This computation produces a new state of the system. 4. The users check the actual results which is produced by the animator with respect to expected results. 5. Steps 2, 3 and 4 are repeated until the users want to stop the animation. Fig.3 illustrates the output of animating the specification of VM in Fig.2. States are
7. Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 25 presented by values of variable itemList, under-specified design decisions must be numCup and amount. For example, the initial introduced. Generally, designs of reactive state of the VM is ({a,b}, (0,0),0). This means systems describe implementation of functions the VM provides two kinds of products namely which realize the observable behaviors a and b. In the initial state, the number of appearing in the specifications. In this product a is 0 and that of product b is also 0. framework, we present the designs of reactive Next, the users enter restock a as a stimulus systems described in appropriate specification sent from the environment. Then, the animator languages - Promela. To verify the design of provides a new state ({a},(1,0),0). In this state, reactive systems, environment models are the number of product a is 1. important; they describe possible entities and behaviors in communication with the target system. The environment model of reactive systems is also presented here. We use a simple example, a vending machine, to demonstrate the specifications, the designs, and the environments of reactive systems. 5.1. Describing design in Promela We assume that the design only defines a set of service functions, it cannot operate by itself. To operate it, we need an environment which Fig.3: Animation of VM's behaviors calls functions of the reactive system. By discharging proof obligations with Therefore, the design needs to be verified in the support of Rodin prover and validating the combination with their environments. We also behaviors with support of animator, we could present the environment model and the show the consistency and sufficiency of the combination model. formal specification. 5. Checking design against formal specification Specifications of reactive systems generally describe the desirable properties and the external behaviors of the systems based on the mathematical data structures using notions of set, relation, and function as mentioned in section 4. Contrarily, the designs present internal behaviors of reactive systems. They show details how to implement the system services. Fig.4: Design in Promela Designs must be close to the Designs of the vending machine can be implementation. The mathematical data straightforwardly described in Promela. The structures must be replaced by the data abstract data structures are replaced by the structures implementable on a computer and implementable data structures, e.g. array,
8. 26 Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 record type. The behaviors are described using The environment defines entities such as items, statements of Promela, e.g. expressions, coins and a sequence of function calls to the target system. assignment statements. The execution of the statement may change the value of variables. Additional variables and constants may be introduced to explicitly describe statements that must be performed to detect cash and credit for computing the total deposited money. Fig. 4 demonstrates a detailed design of the vending Fig.5. Design and Enviroment in Promela machine. In the example, variables having By combining the design and the abstract types in the specification, e.g. itemList environment, we can make a closed system are replaced by variables having concrete types which can operate by itself. We call this a in the design, e.g. ITEM avail[1000]. New combination model. In terms of Promela, a constants are introduced, e.g. CENT is used in combination model can be obtained by the case that a one cent coin is inserted. Design including the Promela code of the design into decisions on how to add a new item into the that of the environment. order set and to remove one from the As explained later, the environment is corresponding position are explicitly described constructed from the specification, and input to based on the implementable data structures and Spin to check the simulation relation. A the control structures, e.g. loop and selection combination of a design and an environment structures. describes the execution of the design according We can see a gap between the specifications and the designs. The observable behaviors to the environment. appearing in the specifications are realized by 5.3. Approach the optimized behaviors appearing in the designs. The specifications can be described in The verification technique used in the a declarative manner whereas the design can be framework is model checking. We check the described in an imperative manner. Our conformance of two models based on the objective is to verify the conformance between simulation relation between them. In particular, such specifications and designs by using a we check whether the design simulates the simulation relation between them. specification. As demonstrated in Fig. 2, the 5.2. Communication of system and specification defines state variables, invariants environment and events which trigger state transitions. Fig. 4 illustrates the overall structure of the Formally, the execution of the specification is design (left) and the environment (right) of the represented as an LTS. Also, Fig. 5 (left) reactive systems. The design defines data describes variables and functions appearing in structures and a collection of inline functions; it the design in Promela. The variables represent cannot operate by itself. To operate it, we need information about the system (states) at certain an environment which calls the functions of the moments. The execution of statements changes target system. Essentially, the reactive systems the values of variables. Therefore, the design need to be verified in the combination with can be interpreted as an LTS if we consider that their environments. the variables are states and each function call is a label to make transitions on the states. In this framework, we apply model checking to verify
9. Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 27 the simulation between two LTSs. Even though the run-time states of the system. Therefore, to there exists a gap between the specification and guarantee some level of correctness of a the design, our framework can verify the reactive system, we need to test it with all many correspondence between state transitions, or as possible the number of sequences of events simulation relation, of the specification and the (test scenarios) together with the possible design. Specifically, each state transition in the values of event parameters. However, the specification leads to a function call, which in number of test cases grows exponentially by the turn triggers multiple state transitions in the length of the events and the size of the design; after these state transitions, the design parameters' domains, so testing reactive reaches a state where the verification conditions systems is challenging. We need an efficient are asserted. and scalable approach to reduce the number of If no counter-example is found, we say the test cases. design conforms to the formal specification For critical reactive systems, their within the input bounds. For more details we requirements are usually specified using formal refer the reader to [11]. notation, e.g. Event-B specifications. In our 6. Verifying implementation against formal framework, we propose a model-based testing specification approach [13] where models are Event-B specifications. Our approach provides system Specification, Design and Implementation is developers a skeleton that can generate test three main artifacts of every software scenarios which contain both input values and development. The specification is the highest expected results. The skeleton acts as a test abstract level description of software. It environment and a test driver that exercises the generally includes desirable properties and system under test (SUT) and reports bugs if the external behaviors of the system. The design is actual results are different from the expected more detailed than the specification. It includes ones. internal behaviors. It is a model of the Of course, there are other techniques such as implementation, that is, it describes a solution model checking or formal verification to to realize the observable behaviors appearing in guarantee some correctness properties of the specification. The implementation is the reactive systems. However, testing is still a most concrete. It is built by realizing the design widely applied in practice, because the formal in concrete programming languages. In section approaches are only applicable for certain 4, we already present an approach to ensure that classes of programs and correctness properties. the design conforms to the specification. This section presents an approach to verify the In particular, our problem statements and implementation against the specification by approach are summarized as follows. Given an applying the model-based testing technique. Event-B specification as shown in Fig.2 and an implementation of a reactive system, also called As mentioned earlier, reactive systems do system under test (SUT) as shown in Fig.6, not operate by themselves but in combination check if all representative behaviors of the with their environments. The stimulus or events specification are correctly implemented in the from the environment trigger the target system's SUT. Here the representative behaviors are the functions or services. Each event may have set of different sequences of events with their additional parameters and may trigger representative input values. additional events. Each event usually changes
10. 28 Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 We know, Event-B model may include 7. Experiments abstract types and infinite range of values. To We have illustrated the specification, the generate sequences of events, firstly, abstract design and the implementation of the vending types in Event-B must be replaced by concrete machine partially in Fig. 2, 4 and 5, types. Also, types having infinite ranges of respectively. In the framework, bounds are set values like Int and Nat must be restricted as for the verification by introducing finite ranges small ranges. This step is to restrict the original of variable values in the Event-B specification. Event-B specification to make a so called In practical applications of the vending specification for test (SfT). The technique that machines, the maximum number of available we use is based on representative values from items is given for each machine. Supposing that equivalence class partitioning, a popular black- a domain knowledge database of vending machines shows 3 kinds of items available for boxed testing technique [13], which is effective customers to be bought such as water, tea, and suitable in our context as we will explain in coffee, and 200 for each. Such kind of vending more details in the next section. Secondly, we machines should accept quarter, dollar as input build a labeled transition system (LTS) of the before selecting any item. Based on this domain state spaces from the restricted specification. knowledge database, we restrict sets as below: Finally, the paths of the LTS are used to build ITEM in {w(water),t(tea),c(coffee)} test cases, which contain both test inputs and PRICE in {$1} expected results for assertions. For more details we refer the reader to [12]. COIN in {Q(QUARTER),D(DOLLAR)} AMOUNT in {$0.25, $0.5, $1} MAXCUP in [0 200] Table 1: Results outputted by Spin These ranges of values are appropriate in present the time taken (s) for the generation. practical applications of vending machines. All Column ``Model Checking'' presents statistics experiments are conducted on Intel (R) Core of the model checker including total actual (TM) i5 Processor at 2.67GHz running memory usage, the time taken (s), and the Windows 10. In verification of the design, verification result in which $\surd$ indicates verification results outputted by Spin are shown the verification has been completed. in Table 1. Here, values in column ``Size of Case No.1 is conducted with number of Ranges'' express bounds of the verification. available items ranging in [0 50]; this allows to Column ``LTS Generation'' shows statistics of restock 10 slots of products and 5 products in the execution sequence generator. Columns each slot. Case No.2 corresponds 20 slots and ``\#State'', and ``\#Trans'' present the number of 10 products in each slot. These ranges are distinct states and that of transitions appearing appropriate in practical applications of the in the execution sequences, each transition vending machines. corresponds to a function call; column ``Time''
11. Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 29 Experiment results of checking the and select item to be bought are not implementation against the formal specification appropriate inputs for dispense item. of VM are shown in Table 2. In all cases of our 8. Discussion experiment, memory usage is minimal (M). Traces of the test show that about 800 This is a highly automatic framework for invocations are tested per second and every software verification. In this framework, we state and invocation are covered in the test. The provide an animator, a generator, and a test test is executed infinitely if no error is detected. driver. Firstly, the animator is used to animate This is due to unlimited nature of reactive the behaviors of the reactive systems; therefore, system, which is caused by unbounded length it supports validating the behaviors of reactive of the test sequences. The test is interrupted systems. Secondly, the generator is used to immediately after the first error is detected and generate the environment and assertions from the test returns a violation assertion. the formal specification. The environment and assertions are then inputted into Spin model Table 2: Results outputted by Test Driver checker for verification of the design. # Systems Mem(Mb) State Arc Result Moreover, the generator is also used to generate Cover. Cover. 1 VM-Ver1 M N/A N/A 1 error test cases and test oracles which are inputs for 2 VM-Ver2 M 100% 100% 0 error verification of the implementation. Finally, the The experiment #1 are executed infinitely. test driver is used to execute test cases on the The experiment #2 returns a violation assertion. implementation and compare to test oracles. Following the trace shown with the error, we From results of case studies presented in could easily detect bugs in implementation of [12] and [13], we found that the framework service select item for Vending Machines. could be straightforwardly applied to verify Memory usage and performance are very good various reactive systems (such as operating to decrease cost of the test. systems, bank ATMs, elevators) where the We asked the engineers to intentionally add designs described in Promela and their formal some bugs into versions of Vending Machine. specifications described in Event-B. Even Then, we test these versions using the same test though this framework has a limitation of the code. All bugs are detected in a short time. model checking; we considered that essential Types of bugs could be detected by our test behaviors of the reactive systems could be still code as below: verified successfully when we use reasonable restrictions for the sets. This shows Conditions enabling services and result of applicability of our framework in verification individual services of SUT is not corrected of reactive systems. with respect to its specification. For example, one version of VM allows the 9. Conclusion customers to select an item when the credit We present an approach for developing and is smaller than the price of the item to be ensuring the quality of software based on the bought. formal specification of requirements. In this Combination of services does not operate framework, we combine animation and theorem correctly with respect to its specification. proving to improve the quality of the formal For example, the results of insert money specification. Therefore, we could easily validate the requirements and ensure the
12. 30 Vũ Diệu Hương / Tạp chớ Khoa học và Cụng nghệ Đại học Duy Tõn 5(48) (2021) 19-30 consistency of the requirements. Based on such Methods in Software Engineering”, Johannes Kepler University Linz. confident formal specification, we apply model [7] Gerard ORegan (2013). Z formal specification checking technique to verify the design and language. In Mathematics in Computing, apply testing technique to verify the pages 109{122. Springer London. implementation. We provide an animator, a [8] Gerand J. Holzmann (2004). The SPIN Model Checker – primer and reference manual. Addison – generator and a driver to automate steps in this Wesley. framework. This framework adapts to overall [9] R. Venkatesh, U. Shrotri, G. M. Krishna and S. software development processes such as Agrawal (2014), "EDT: A specification notation for waterfall, evolution model, agile methods. This reactive systems". Design, Automation & Test in Europe Conference & Exhibition, pp. 1-6, doi: makes it possible to systematically ensure the 10.7873. quality of reactive systems based on the [10] J. Fernandes, J. B. Jứrgensen, S. Tjell (2007). confident specification with high automation, Requirements Engineering for Reactive Systems: Coloured Petri Nets for an Elevator Controller. The adaptation, and practicality. 14th Asia-Pacific Software Engineering Conference References (APSEC’07). [11] Dieu-Huong Vu, Yuki Chiba, Kenro Yatake, [1] G. Klein, J. Andronick, K. Elphinstone, G. Heiser, Toshiaki Aoki (2015). A Framework for Verifying D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. the Conformance of Design to Its Formal Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Specifications. IEICE Trans. Inf. Syst. Vol.98-D, Winwood (2010). seL4: Formal verification of an no.6, pp.1137—1149. operatingsystem kernel,” Communications of the [12] Dieu Huong Vu, Anh Hoang Truong, Yuki Chiba, ACM, vol. 53, no. 6, pp. 107– 115. Toshiaki Aoki (2017). Automated testing reactive [2] M. Leuschel and M. Butler (2008), “ProB: An systems from Event-B model. 4th NAFOSTED automated analysis toolset for the B method,” Conference on Information and Computer Science, International Journal on Software Tools for 2017, pp. 207-212, doi: Technology Transfer, vol.10, no.2, pp.185– 10.1109/NAFOSTED.2017.8108065. 203. [13] Frederic Dadeau, Kalou Cabrera Castillos, and [3] P. Matos, B. Fischer, and J. Marques-Silva (2009), Regis Tissot (2012). Scenario based testing using “A lazy unbounded model checker for Event-B,” in symbolic animation of B models. Software Testing, Formal Methods and Software Engineering, Lecture Verification and Reliability, 22(6):407-434. Notes in Computer Science, vol.5885, 485-503, [14] Nadeem Akhtar, Malik M. Saad Missen (2014). 2009. Contribution to the Formal Specification and [4] M.P.E. Heimdahl and D. George (2004). Test-suite Verification of a Multi-Agent Robotic System. reduction for model based tests: effects on test European Journal of Scientific Research ISSN 1450- quality and implications for testing. Proceedings of 216X / 1450-202X Vol.117 No.1, pp. 35-55. the 19th IEEE International Conference on [15] Phillip A. Laplante (2017). Requirements Automated Software Engineering. Linz, Austria Engineering for Software and Systems. ISBN [5] Jean-Raymond Abrial (2010). Modeling in Event-B: 9781138196117 by Auerbach Publications. 400 system and software engineering. Cambridge Univ Pages 95 B/W Illustrations. Press. [16] Luca A., Anna I., Kim G. L., and Jiri S (2011). [6] Andreas Muller (2009). VDM the vienna Reactive system modeling specification and development method. Bachelor thesis in ”Formal verification. Cambridge University Press. ISBN 978051181410.