Verification of temporal properties of infinite state systems

Verification of temporal properties of infinite state systems Author: Cristina Luengo Agulló Director: Albert Rubio Degree in Computer Science Computing specialization Universitat Politècnica de Catalunya Facultat d’informàtica de Barcelona 29 June 2015 Abstract It is no secret that computer software programs, computer hardware designs, and computer systems in general exhibit errors. Testing and simulation methods can identify many significant problems, but for systems that have safety or economically critical requirements, exhaustive verification is indispensable. Such exhaustive analysis can be performed with the use of formal verification methods. One approach to formal verification is model checking, which is a fully automated process based on the construction of abstract models to represent systems. These models are then checked against desired properties defining a specification, usually expressed in some temporal logic, such as linear temporal logic (LTL). Temporal properties can describe the ordering of events in time without introducing time explicitly, thereby being useful when verifying the possible executions of a system. This project aims to implement model checking algorithms that determine whether an LTL formula expressing a desired property is satisfied in a computing system. Resumen No es ningún secreto que tanto los sistemas software como hardware generalmente presentan errores. Los métodos de testeo y simulación pueden identificar muchos problemas importantes, pero para sistemas que tienen requerimientos de seguridad o que son económicamente críticos, es indispensable llevar a cabo una verificación exhaustiva. Tal análisis se puede realizar utilizando métodos de verificación formal. Un enfoque de la verificación formal es la verificación de modelos, que es un proceso totalmente automático basado en la construcción de modelos abstractos para representar sistemas. Posteriormente, sobre estos modelos se comprueban propiedades deseadas del sistema, normalmente expresadas en alguna lógica temporal, como por ejemplo lógica linear temporal. Las propiedades expresadas con fórmulas de lógica linear temporal pueden describir el orden de los eventos en el tiempo sin describir el tiempo explícitamente. Por eso mismo, son útiles a la hora de verificar las posibles ejecuciones de un sistema. Este proyecto pretende implementar algoritmos de verificación de modelos que determinen si una fórmula de lógica linear temporal que exprese una propiedad de un cierto sistema es satisfecha por éste. Resum No és cap secret que tant els sistemes software com hardware generalment presenten errors. Els mètodes de testeig i simulació poden identificar molts problemes importants, però per sistemes que tenen requeriments de seguretat o que són econòmicament crítics, és indispensable realitzar una verificació exhaustiva. Aquest anàlisi es pot fer utilitzant mètodes de verificació formal. Un enfocament de la verificació formal és la verificació de models, que és un procés totalment automàtic basat en la construcció de models abstractes per representar sistemes. Posteriorment, sobre aquests models es comproven propietats desitjades del sistema, normalment expressades en alguna lògica temporal, com per exemple la lògica lineal temporal. Les propietats expressades amb fórmules de lògica lineal temporal poden descriure l’ordre dels esdeveniments en el temps sense descriure el temps explícitament. Per això mateix, són útils a l’hora de verificar les possibles execucions d’un sistema. Aquest projecte pretén implementar algorismes de verificació de models que determinin si una fórmula de lògica lineal temporal que expressi una propietat d’un cert sistema és satisfeta per aquest. Acknowledgements First and foremost, I would like to thank my project director, Albert Rubio. Working alongside with him has not only been an enriching experience, but also a fun time. His enthusiasm for research and for the work that he does is truly inspiring, and this translated to motivation for me throughout the project. I can say that I have learned many new things while doing this project, and I always had full support from him when struggling with something. I would also like to thank Alicia Villanueva and Laura Titolo for providing us with examples to test. Finally, I would specially like to thank Javi as well, who always supported me and helped me with the design of this document. 1 Contents Abstract............................................. 1 Resumen ............................................ 1 Resum.............................................. 1 1 Introduction 6 1.1 Motivation ........................................ 6 1.2 Context .......................................... 7 1.2.1 Automated formal verification . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.2.2 Automatatheory................................. 7 1.3 Stateoftheart...................................... 8 1.3.1 LTL model checking for finite-state systems . . . . . . . . . . . . . . . . . . 8 1.3.2 LTL model checking for infinite-state systems . . . . . . . . . . . . . . . . . 9 1.4 Projectcontribution ................................... 10 1.5 Projectoutline ...................................... 10 2 Project management 11 2.1 Objectives......................................... 11 2.2 Obstacles ......................................... 11 2.3 Scope ........................................... 12 2.3.1 Methodology ................................... 13 2.4 Planning.......................................... 14 2.4.1 Descriptionoftasks ............................... 14 2.4.2 Temporalplanning................................ 16 2.4.3 Deviations..................................... 18 2.4.4 Resources..................................... 18 2.5 Budget........................................... 19 2.5.1 Directcosts.................................... 19 2.5.2 Indirectcosts................................... 20 2.5.3 Unforeseencosts ................................. 21 2.5.4 Totalbudget ................................... 21 2.6 Sustainabilityanalysis .................................. 22 2.6.1 Economic sustainability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.6.2 Environmental sustainability . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.6.3 Social sustainability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 2 3 Preliminaries 24 3.1 Lineartemporallogic................................... 24 3.2 Formal languages and automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.2.1 FiniteAutomaton ................................ 26 3.2.2 Büchiautomaton................................. 27 3.2.3 Transition-based generalized Büchi automaton . . . . . . . . . . . . . . . . 28 3.3 TransitionSystem .................................... 28 3.3.1 Finite-statesystems ............................... 29 3.3.2 Infinite-state systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 4 Satisfiability of LTL formulas 31 4.1 Parsingtheformulas................................... 32 4.2 Automaton transformation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4.2.1 Formularewriting ................................ 32 4.2.2 LTLtoTGBA .................................. 33 4.2.3 Degeneralization ................................. 38 4.3 Emptinesstest ...................................... 40 4.4 Experiments........................................ 41 4.4.1 LTL over linear integer arithmetic expressions . . . . . . . . . . . . . . . . . 41 5 Verification of LTL properties of computing systems 45 5.1 Büchi Automaton intersection . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 5.2 Verification ........................................ 51 6 Conclusions 53 7 Future work 54 Bibliography 55 3 List of Tables 2.1 Identification of the requirements . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2 Tasksbreakdown..................................... 17 2.3 Tasks and hours assignment for each role . . . . . . . . . . . . . . . . . . . . . . . 19 2.4 Humanresourcesbudget................................. 20 2.5 Hardwareresourcescosts ................................ 20 2.6 Softwareresourcescosts ................................. 20 2.7 Electricity and paper costs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 2.8 Unforeseencosts ..................................... 21 2.9 Totalcosts ........................................ 21 2.10Sustainabilitymatrix................................... 23 4.1 Definition of New and Next for non-literals . . . . . . . . . . . . . . . . . . . . . . 36 4.2 Examplesofformulas................................... 42 4 List of Figures 1.1 Automatonexample ................................... 8 2.1 System and property automatons that model the behavior of a switch. . . . . . . . 12 2.2 Intermediate representation of ¬stop U(distance < threshold)........... 15 2.3 Büchi automaton for the formula ¬stop U(distance < threshold).......... 16 2.4 Gantt chart defining the project planning . . . . . . . . . . . . . . . . . . . . . . . 17 3.1 Automatonexample ................................... 26 3.2 Büchi automaton for the formula (received →♦processed)............ 27 3.3 TGBA for the formula (received →♦processed).................. 28 3.4 Transition System for counter system . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.5 Transition system for program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.1 Nodesplitting....................................... 36 4.2 Degeneralizer for a TGBA with one accepting set . . . . . . . . . . . . . . . . . . . 39 4.3 Degeneralizer for a TGBA with two accepting sets . . . . . . . . . . . . . . . . . . 39 4.4 TGBA representing pUq................................ 40 4.5 Büchi automaton representing pUq.......................... 40 4.6 Büchiautomatonexample................................ 41 4.7 Examples of Büchi automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 5.1 Modelcheckingoutline.................................. 46 5.2 Büchi automaton A1(left) and A2(right) ....................... 47 5.3 Büchi automaton Arepresenting A1∩A2(regular intersection) . . . . . . . . . . . 47 5.4 Büchi automaton Arepresenting A1∩A2....................... 48 5.5 Büchi automaton Arepresenting A1∩A0 2....................... 48 5.6 Computing system (left) and Büchi automaton for the formula (j > i)U(j=i) (right)........................................... 49 5.7 Transition system for the program . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 5.8 Intersection between transition system and Büchi automaton . . . . . . . . . . . . 51 5.9 Transition System example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 5 the process and implementing it. Further detail on the actions taken to face or adapt to these obstacles can be found in Section 2.4.3. 2.3 Scope As explained in Section 1.3.1, LTL formulas specify properties that vary over time, so we can use them to express the desired behavior of a system during its execution. Model checking consists in the verification of those formulas on computing systems, and it requires the creation of abstract models for both the systems and LTL formulas. In order to build those models, we will base our implementation in the fact that transition systems can be used to represent computing systems, and to model LTL properties we can use automata on infinite words, namely Büchi automata. This type of automata has great expressive power, and yet its emptiness can be checked fairly efficiently, which will be of great use when checking the satisfiability of LTL formulas (see Sections 3and 4for more details). Example 1. The transition system and Büchi automaton in Figure 2.1 are models of a system representing a switch, and an LTL formula (on →♦off)which specifies that whenever the switch is on, it will eventually go off. An execution will be defined by a sequence of labels of the reachable transitions at each state (e.g. sequence on →off →on in the system model). Therefore, LTL models will represent executions of the system with the desired behavior, and system models will express all possible executions. start on off start on ∧ ¬off ¬on ∨off off ¬off Figure 2.1: System and property automatons that model the behavior of a switch. Once the models are obtained, we consider two possible approaches in order to apply model checking methods to verify LTL properties on computing systems. The first one is by trying to verify formulas directly created from computing systems (e.g. from software programs). In such case, it would be enough to check whether the given LTL formulas are valid, thereby confirming that the systems they represent meet the desired properties. Our approach in this case will be to use LTL satisfiability in order to check the validity of the given formulas (see Section 4for more details). On the other hand, the second approach consists in adapting the model checking method for finite-state systems to infinite-state systems. In order to do so, given a model Mfor a system and a Büchi automaton Bϕmodeling an LTL property ϕover the system, it is necessary to perform T=M∩B¬ϕ. Later on, the transition system Tcan be fed to a program analysis tool, which will check whether M|=ϕby analyzing T. However, this is beyond the scope of this project and we will only be concerned with the generation of transition systems resulting from the intersection. 12 Considering the process described, the different functionalities we will implement are the following: •Specification of LTL formulas: Users will be able to specify LTL formulas, either coming from software programs or directly embedded in the parts of the computing system they want to verify. •Visual output of the models: In order to obtain more feedback about the verification process, users will be able to see the system and property models, and if necessary, the resulting automaton of their intersection. •Satisfiability feedback: Our tools will provide results for the satisfiability of LTL formulas. These functionalities are part of the functional objectives defined for our project, and are also an important requirement. Table 2.1 shows the identification of the requirements in relation to the life cycle of the project. Life cycle Project value Planning Implementation Experimentation Closing Cost Human resources Hardware resources costs costs Time Start: End: 09-02-2015 29-06-2015 Functional objectives LTL formulas specification Models visual output Satisfiability feedback Quality Possible optimizations Risks Non-scalable Table 2.1: Identification of the requirements 2.3.1 Methodology For the development of this project we followed a rigorous methodology which helped us carry out the different tasks incrementally and more efficiently. We started out by implementing the parts that worked as a basis for other parts, and did not move on to a new task until the previous one was completed and validated. The different stages we followed are listed below in order: 1. Parsing LTL formulas: We defined a method to read input LTL formulas and represent them using an internal structure of the parsing algorithm, which helped us transform them into a Büchi automaton later on. 2. LTL to Büchi automaton: Once the formulas could be parsed, we were able to build models for them in the shape of Büchi automata. 13 3. Visualization methods: In order to check the automatons built and be confident about their correctness, we implemented visualization methods using the dot library. 4. Emptiness test: To determine whether the language accepted by a Büchi automaton is empty, we implemented an emptiness test. This allowed us to check the satisfiability of LTL formulas (see Section 4). 5. Büchi automata intersection: We implemented a method to intersect transition systems with Büchi automata. This allowed us to obtain results which later on would be fed to a program analysis tool in order to verify LTL properties on computing systems (see Section 5). The methodology was based on setting short cycles, where we aimed to achieve a certain goal related to the stage we were in. Therefore, we had weekly meetings to discuss the goals that were planned, and the outcome of the weeks compared to the initial planning. This is similar to the SCRUM methodology. This methodology allowed us to have regular control over the different phases of the project, and prevent or solve deviations at an early stage. Moreover, a version control tool was used to keep track of all the different versions of the project that we implemented. 2.4 Planning In this section, we summarize our temporal planning for the development of the project. This project was carried out in a time frame of five months approximately, starting on the 2nd of February 2015 and finishing on the 29th of June 2015. The following sections describe the breakdown of tasks, the general time planning, resources used, and the deviations that occurred while developing the project. 2.4.1 Description of tasks Some general tasks have been defined in order to sum up the different steps of the project regarding the organization and implementation. Their definition and detailed explanations will be given in the following sections. Project definition This comprises the definition of the subject for the project. An initial stage of research in the LTL verification field was carried out in order to decide whether the project would be viable. And indeed, after documenting ourselves we came to the conclusion that the project would be viable and interesting to develop. Furthermore, we decided that we were going to use some already working verification tools to model the computing systems. Project management It involves the project description, project planning, control meetings and bureaucratic tasks. •Project description and planning: It constitutes all the GEP tasks. These include from the description of the project, its scope and resources needed, to a state of the art research and budget calculation. This stage helped us have a better overview of what was necessary to develop the project and also, organize the tasks so it could be done in the stipulated time. 14 •Control meetings: As described in Section 2.3.1, we kept control of the evolution of the project by regularly meeting to discuss the situation at each stage. This practice allowed us to adapt our planning better and prevent critical deviations. •Bureaucratic tasks: They comprise the project inscription, the GEP submission, the final presentation inscription and the final submission of the project. Environment set up Before we could start implementing the project, we needed to install the required software. A list of all the software needed is provided in Section 2.4.4. Main development The following tasks comprise the implementation of the project. •Parsing of LTL formulas: LTL formulas will determine desired properties of a system, so we needed a way to save and represent formulas provided by the user. Therefore, this task involved programming in C++ and also using the F lex and Bison utilities, which generate a scanner and a parser algorithm. These read the LTL formulas and build an intermediate representation for them, respectively. Example 1. Consider a system modeling the behavior of a robot. One possible property to verify could be that the robot does not stop until the distance to an obstacle is less than a given threshold. Such property would be modeled by the LTL formula ¬stop U(distance < threshold) And the corresponding intermediate representation would be the Abstract Syntax Tree (AST)- like structure shown in Figure 2.2. U ¬ stop < distance threshold Figure 2.2: Intermediate representation of ¬stop U(distance < threshold) •Generation of Büchi automata: It comprises the implementation of algorithms that build Büchi automata from LTL formulas, and adapt a system model to a Büchi automaton representation. This involved C++ programming and looking for a visualization tool that could show the results in a more readable way. Example 2. Following Example 1, Figure 2.3 shows the Büchi automaton for the formula ¬stop U (distance <threshold). This automaton accepts all executions where the robot does not stop if it is far enough from an obstacle. 15 0start 1 distance < threshold ¬stop true Figure 2.3: Büchi automaton for the formula ¬stop U(distance < threshold) •Emptiness check: This test is performed on a Büchi automaton in order to determine if the language it accepts is empty. If the automaton comes from an LTL formula ϕmodeling a program, then checking the satisfiability of ¬ϕwill determine whether the formula is satisfiable. If that is the case, the LTL property has been verified on the system. •Intersection of Buchi automata: The intersection of Büchi automata is performed in order to obtain a combined model from the computing system and LTL property models. This resulting model could then be fed to a program analysis tool in order to check the satisfiability of the LTL property on the system. Development control These tasks were carried out at the end of every development task. •Validation: Our implementation was validated after each development task finished, thereby avoiding the propagation of errors to subsequent stages. •Technical documentation: Documentation was written as implementation tasks finished, and it was extended once the implementation of the project was done. Experimentation A stage of experimentation was carried out in order to assess the performance of our tools with different kinds of LTL formulas. Final stage This stage was used to gather everything up and finish the technical report, as well as preparing the final presentation. The following sections describe the temporal planning followed for the development of the project. 2.4.2 Temporal planning In this section we describe how the temporal planning was organized, the deviations we had to face during the implementation phase, and the resources needed when developing the project. Timetable Table 4.1 shows the breakdown of tasks along with the estimated hours spent in each task, their dependencies, and the resources needed to carry them out. The dependencies between tasks are finish to start, except for tasks 8, 9 and 10, which were performed once an implementation task 16 (i.e. tasks 4-7) was done. The hours allocated for those tasks are the total sum of hours spent at each implementation stage. Tasks Time (hours) Dependencies Resources 1 Project definition 5 — — 2 Project description and planning 70 1 — 3 Environment set up 5 2 H1 4 Parsing of LTL formulas 40 3 S1, S2, S3, S7, H1 5 Generation of Buchi automatons 90 4 S1, S2, S4, S6, S7, H1 6 Emptiness check 60 5 S1, S2, S4, S7, H1 7 Intersection of Buchi automatons 70 5 S1, S2, S4, S5, S7, H1 8 Experimentation 30 6, 7 S1, S2, S4, S7 H1 9 Validation 30 4, 5, 6, 7 1S1, S2, S4, S7, H1 10 Technical documentation 70 4, 5, 6, 7, 8 S8, H1 11 Control meetings 20 — — 12 Final stage 30 8 S8, H1 Total 520 Table 2.2: Tasks breakdown As can be seen, most of the hours are allocated to implementation tasks, since they comprise the main part of the project. Gantt chart Figure 2.4 shows the final Gantt chart. Task 1 was omitted for better visualization, since it was carried out a month earlier than all the other tasks. Tasks 9 and 10 are broken down into smaller tasks for better understanding, since they were performed right after the corresponding tasks they depended on finished. The amount of hours dedicated to the project per day was of about five hours on average, and we consider working days. Figure 2.4: Gantt chart defining the project planning 1Validation and technical documentation was done at the end of each indicated task. 17 2.4.3 Deviations We started performing the tasks according to the initial planning until the implementation of the LTL to Büchi automaton transformation task. During this task, we had to face the following problems: •Conceptual complexity of the algorithm: The algorithm chosen had some parts that were difficult to understand, so an extra effort was needed when developing those parts. •The algorithm does not scale well: While for small formulas we could obtain correct and fast results, for bigger formulas there was a blowup in the execution time of the algorithm. This is due to the fact that the size of the automata generated is exponential in the size of the LTL formula. Thus, the bigger the formula the more calculations need to be done. On one hand, the first problem was solved by doing research on the topic and finding other sources of information. Once we had a clear idea of how all the components worked and we fully understood the algorithm, we finished the implementation. On the other, the second problem was harder to tackle, since we could not avoid the fact that bigger formulas involve more computations, thereby leading to larger execution times. Hence, we contemplated two possible options: either trying to optimize the algorithm by reusing calculations, or trying another algorithm with a different approach. But since we had already implemented the algorithm, we decided to carry out the optimization. However, it did not show any improvement in the execution times, so we proceeded to the next task and decided to leave the optimizations for the final stage. The next task we carried out after that task was the emptiness check, rather than the intersection of Büchi automatons. This alteration on the original planning was done because after doing some research, we assumed that it could be done in less time than the stipulated. Thus, we could have a better overview of the time we had left if we finished that task before expected. 2.4.4 Resources We needed the following software and hardware resources to develop the project: Software S1. Ubuntu 14.04: Used in all tasks S2. Emacs: Editor used to program in C++. Used in all tasks. S3. Flex and Bison: Programs needed for the LTL formulas parsing. S4. Visualization tool: We used the dot tool. S5. VeryMax: Used for building transition systems. S6. BarceLogic: Used when building Büchi automata. S7. Subversion: Used in all tasks to keep track of the versions of the project. S8. L A T EX: Used for project documentation. 18 Hardware H1. PC: Used in all tasks. 2.5 Budget In this section we estimate the budget for the project considering the different tasks that were carried out and the resources needed. Even though there were some deviations in the implementation phase, the estimation of costs is the same that we initially performed, since those deviations did not affect the budget. We contemplate the direct, indirect and unforeseen costs associated to the project. 2.5.1 Direct costs These costs are directly related to the development of the tasks described in Section 2.4.2. Therefore, they are computed considering the different resources needed to carry out the project, which are introduced in the following sections. Human resources The different roles that participated in the development of the project were: 1. Project Manager: Responsible for establishing the project plan and coordinating resources to complete the plan on time and budget. 2. Software designer: Helps creating software that meets the client’s needs, in an effective and cost-efficient manner. 3. Software developer: Responsible for the technical implementation of the software. Considering the tasks described in Section 2.4.1, the assignment of tasks for the different roles and the budget allocated for them is shown in tables 2.3 and 2.4, respectively. Tasks Hours Role 1 Role 2 Role 3 1 Project definition 5 5 — — 2 Project description and planning 70 70 — — 3 Environment set up 5 — — 5 4 Parsing of LTL formulas 40 — 10 30 5 Generation of Büchi automatons 90 — 30 60 6 Emptiness check 60 — 15 45 7 Intersection of Büchi automatons 70 — 25 45 8 Experimentation 30 — — 30 9 Validation 30 — 15 15 10 Technical documentation 70 — 35 35 11 Control meetings 20220 20 20 12 Final stage 30 10 10 10 Total 520 105 160 295 Table 2.3: Tasks and hours assignment for each role 19 Role Hours Price per hour Cost Project Manager 105 50 ¤5.250 ¤ Software designer 160 35 ¤5.600 ¤ Software developer 295 35 ¤10.325 ¤ Total 21.175 ¤ Table 2.4: Human resources budget Hardware resources The only hardware resource we needed was a computer, so the estimated cost for hardware is the one associated to the depreciation, which is computed as follows: 4years ×12 months/year ×20 days/month ×5hours/day = 4800 hours Depreciation = (1000 ¤/4800 hours)×520 hours = 108,33 ¤ The results are summarized in Table 2.5. Product Price Useful life Usage Depreciation Computer 1000 ¤4 years 520h 108,33 ¤ Total 108,33 ¤ Table 2.5: Hardware resources costs Software resources The cost for software resources is described in table 2.6. Since we will use open-source software, no costs will be associated to it. Product Price Ubuntu 14.04 0 ¤ Emacs 0 ¤ Flex and Bison 0 ¤ Visualization tool 0 ¤ L A T EX 0 ¤ Total 0 ¤ Table 2.6: Software resources costs 2.5.2 Indirect costs Other resources unrelated to the project were also needed for its development and hence, must be considered in the budget as well. Table 2.7 shows the indirect costs associated to electricity and paper. 2Each role is assigned the total amount of hours dedicated to this task, since everyone will participate in the meetings. Therefore, the total sum of hours allocated to the roles will be different than the total sum of hours dedicated to the tasks. 20 On one hand, we assumed that the computer consumed in average 250 W per hour, so the total energy that it consumed during the project (520 hours) was energy = 250W×520h= 130 kWh. The rest of the energy (32 kWh) was consumed by electricity. Product Price Units Cost Electricity 0.12 ¤/kWh 162kWh 19,44 ¤ Paper 4,5 ¤/pack ¤500 4,50 ¤ Total 23,94 ¤ Table 2.7: Electricity and paper costs 2.5.3 Unforeseen costs This section includes the costs associated to unexpected events that might have increased the price of the project. We consider them here because they were part of the initial budget estimation. We contemplate one possible scenario which would have slightly deviated the budget. 1. The computer needing repair: Since the computer we will use was purchased a few months before starting the project, we will assign a probability of 5% to this event. Table 2.8 shows the resulting costs. Event Probability Price Cost 1 5% 200 ¤10 ¤ Total 10 ¤ Table 2.8: Unforeseen costs 2.5.4 Total budget The total estimated budget for the project is defined in table 2.9. A 5% level of contingency is added in order to contemplate possible deviations not considered in unforeseen costs. Type Cost Human resources 21.175 ¤ Hardware resources 108,33¤ Software resources 0 ¤ Total direct costs 21.283,33 ¤ Paper & Electricity 23,94 ¤ Total indirect costs 23,94¤ Total unforeseen costs 10 ¤ Contingency 1.062,86 ¤ Total 22.383,13 ¤ Table 2.9: Total costs 21 3.2.3 Transition-based generalized Büchi automaton Formally, a transition-based generalized Büchi automaton is a 5-tuple TGBA = < Q, Σ,∆, q0, F >, where: Q: A finite set of states Σ: A finite set of labels ∆: A transition relation, Q×Σ→Q q0: The initial state, q0 Q F: A set of sets of accepting transitions, F⊆2∆ An infinite word wover the alphabet Σis accepted by a TGBA if and only if there exists an infinite execution of the TGBA on wthat contains at least one transition from each accepting set of the sets in Fan infinite number of times. If F=∅then a word wis accepted if and only if there exists and infinite execution of the TGBA on w. Example 5. Following Example 1, Figure 3.3 shows the TGBA that accepts all the words that satisfy the formula (received →♦processed). Note that in this case, F={{τ1, τ4}}, and for better visualization transitions labeled with a {0} belong to the only set of F. Therefore, an execution on the automaton is accepted if and only if it goes through at least one of the transitions labeled with {0}infinitely often. q1 start q2 τ1:¬received ∨processed,{0} τ3:received ∧ ¬processed τ2:¬processed τ4:processed,{0} Figure 3.3: TGBA for the formula (received →♦processed) So far, we have introduced how LTL properties can be modeled. Next section describes how computing systems can be modeled with the use of Transition Systems. 3.3 Transition System A Transition System is a 3-tuple TS =< S, R, I > where: S: A finite set of states R: A transition relation, R⊆S×S I: A finite set of initial states, I⊆S Transition systems are used to describe dynamic processes with configurations representing states, and transitions saying how to go from one state to another. Therefore, a transition system generates a set of sequences of labels from its transitions, which describe all the possible execution paths of the system it is modeling. They can be used to model either finite-state or infinite-state systems, with slight variations. 28 3.3.1 Finite-state systems Finite-state systems rely on bounded domains in order to represent computer systems. These domains are obtained through finite abstractions, which apply a limit on the number of elements the state space has. For instance, if a system had to deal with integer numbers, one possible abstraction would be to use only a subset (e.g. 32-bit numbers). Therefore, these systems provide an explicit representation of the state space, meaning that they enumerate every possible state change the system could perform. Example 1. Consider a system modeling a counter between 0 and N, which increments and decrements. An explicit representation of such system for N= 3 is shown in Figure 3.4. As can be seen, the domain is bounded to D={0..N}, and there is a state for each increment/decrement of the counter. 0start 1 2 3 inc inc inc decdecdec Figure 3.4: Transition System for counter system Since transition systems can define infinite traces, they can be considered Büchi automata where all states are accepting states. Intuitively, a transition system defines all the possible executions of a system, so any infinite run in the transition system would be an accepted run. Moreover, those transition systems that do not represent infinite paths can be turned into Büchi automata by adding self-loops to ending states, which do not change to another state anymore. 3.3.2 Infinite-state systems As seen in the previous section, finite-state systems need to bound their domain through finite abstractions. This clearly imposes a limit on the power of representation transition systems can provide when modeling computer systems. For instance, following Example 1, if we had to represent a system which performs an undefined number of increments/decrements, it would not be possible to use the representation given. Moreover, if a system needed to perform a huge amount of increments, the state space of the model would increase dramatically. On the other hand, infinite-state systems do not impose a bound on their state space domain. Hence, they allow one to represent more complex systems, such as software programs manipulating integer variables. Such systems require more general models which, for instance, admit the representation of assignments between variables. Example 2. Figure 3.5 shows an example of a program manipulating integer variables and a transition system representing it. 29 int main() { int x=undet(),y=undet(),z=undet(); l1: while (y>=1) { x--; l2: while (y<z) { x++; z--; } y=x+y; } } Figure 3.5: Transition system for program As can be seen, transitions of the transition system have two parts: conditions and assignments. The former determine whether a transition can be activated, and the latter express the changes variables x,yand zexperiment once the transition is fired. Hence, primed variables indicate the new values of x,yand zafter the transition is activated, and unprimed ones represent their values before the transition, as explained in [23]. Moreover, initial states have one or more associated entry transitions which are applied to the initial values, before reaching the initial location. In example of Figure 3.5, the only initial location is 11, which has a single entry transition with condition true and no assignments. 30 Chapter 4 Satisfiability of LTL formulas In this section we introduce a method to check the validity of LTL formulas through LTL satisfiability. An LTL formula is valid if every possible interpretation is a model (i.e. satisfies the formula). Formally, given an LTL formula ϕdefined over a set of propositions AP , the formula specifies a language L(ϕ) = {σ|σ  (2AP )w:σ|=ϕ}with all the traces that satisfy it. Thus, ϕis valid if and only if all possible interpretations of ϕbelong to L(ϕ), that is: (2AP )w=L(ϕ) Such condition implies checking that all the elements of (2AP )ware contained in L(ϕ). To this end, we can check the satisfiability of ¬ϕ. Intuitively, if ¬ϕhas a model, this means that there is an interpretation that does not satisfy ϕ(as it satisfies ¬ϕ), and thus ϕis not valid. This can be performed by checking whether the language defined by ¬ϕis empty. If that is the case, there will be no interpretations that satisfy ¬ϕ, and ϕis proven to be valid. Formally: ϕ≡true ↔L(¬ϕ) = ∅ One way to check whether L(¬ϕ) = ∅is by using a Büchi automaton that accepts the words in L(¬ϕ). Once the automaton is built, it is possible to perform an emptiness test in order to see whether the language it accepts is empty or not. Therefore, the steps to follow are: 1. Negate the formula 2. Translate from LTL to Büchi automaton 3. Perform an emptiness test The following sections describe how we parse an LTL formula ϕ, translate ¬ϕinto a Büchi automaton and perform the emptiness test on the latter in order to check the satisfiability of ¬ϕ (i.e. the validity of ϕ). 31 4.1 Parsing the formulas The first step is to parse the LTL formulas specified by the user in the system code. LTL properties will be specified as code statements among the system’s source code. Hence, they will be evaluated in the point where they are inserted, rather than globally for the whole system. We will use the Flex and Bison utilities to parse the formulas and will save and represent them with an Abstract Syntax Tree (AST) structure. Once the formulas are parsed, the Büchi automaton representing each formula will be built following the method introduced in the following section. 4.2 Automaton transformation As stated in Section 3.2, given an LTL formula φdefined over a set of propositions AP, it is possible to build a Büchi automaton representing such formula. The transition labels of the automaton will be propositional formulas over AP, and they will possibly represent multiple elements of 2AP . Example 1. For AP ={a, b}and Σ = 2AP , the label true would correspond to any of the elements of Σ(i.e: {a},{b},{a, b}), the label awould correspond to either {a}or {a, b}, and the label ¬a∧bwould correspond to {b}. Therefore, transition labels on the Büchi automaton will determine the propositions that need to be true for a transition to be activated, regardless of the value of the other propositions. This means that a run in the Büchi automaton will be an infinite sequence of interpretations over AP that will make the LTL formula satisfiable. Note that the size of the generated Büchi automaton might be exponential in the size of the LTL formula, as explained in [24]. Hence, Büchi automata can end up being huge, depending on the formulas they are generated from. For the translation, there are different approaches in the literature [25,26], but the algorithm used in this project is based in that of [13,27], and it is carried out in the following steps: 1. Formula rewriting. 2. Transformation of the formula into a TGBA. 3. Degeneralization of the TGBA to obtain a Büchi automaton. The first step is performed in order to obtain smaller automata and simplify the transformation algorithm by using less temporal operators. The second one takes into consideration eventualities introduced by Uformulae, and the third generates the resulting Büchi automaton. Each step is explained in the following sections. 4.2.1 Formula rewriting Formulas will be rewritten into their Negation Normal Form (NNF), where the negation operator ¬is only found in front of propositions. 32 Example 2. Let pand qbe propositions. Examples of the Negation Normal Form of LTL formulas are: ¬p=♦¬p¬(X p)=X¬p ¬♦p=¬p¬(p∧q) = ¬p∨ ¬q ¬(pUq) = ¬pR¬q¬(p∨q) = ¬p∧ ¬q ¬(pRq) = ¬pU¬q Furthermore, the only operators that will be used are U, R, ∨and ∧, since the other ones can be derived from these (see Section 3.1). In order to avoid an exponential blow up in the size of the formula rewritten, we will consider both U and R, even though they can be derived from each other. In addition to that, we have also implement a simplification step using the following rewriting rules introduced in [13,27]. Let φ,ψand ϕbe LTL formulas. The rewriting rules applied are: φ∧φ→φ X true →true φ∧true →φ φ Ufalse →false φ∧false →false (♦ φ)∨(♦ ψ)→♦(φ∨ψ) φ∧ ¬φ→false ♦X φ →X♦φ φ∨φ→φ♦ φ→♦ φ φ∨true →true ♦♦ φ→♦ φ φ∨false →φ X♦ φ→♦ φ φ∨ ¬φ→true ♦(φ∧(♦ ψ)) →(φ)∧(♦ ψ) (Xφ)U(Xψ)→X(φUψ)(φ∨( ♦ ψ)) →(φ)∨(♦ ψ) (φRψ)∧(φRϕ)→φR(ψ∧ϕ)X(φ∧♦ ψ)→(X φ)∧(♦ ψ) (φRψ)∨(ϕRψ)→(φ∧ϕ)Rψ X(φ∨♦ ψ)→(X φ)∨(♦ ψ) (Xφ)∧(Xψ)→X(φ∧ψ)Rψ 4.2.2 LTL to TGBA Given an LTL formula ϕ, the algorithm relies on the construction of an intermediate graph of nodes that somehow contain subformulae of ϕ. Transitions and states of the TGBA come from the nodes of such temporal graph, and the algorithm returns the TGBA generated. Intuitively, a transition in the TGBA will determine the literals 1that hold at a given moment in time, and a state will represent formulae that hold on an execution starting from it. Therefore, during the TGBA construction, a node will keep information about the formulas that must be satisfied in the current step, and formulas that must be satisfied from the next step in time on. So, in the end, all intermediate nodes are processed and some of them provide transitions and states of the TGBA. The algorithm will create and expand nodes by applying recursive rules that decompose subformulae of ϕ. These are based on LTL semantics (see Section 3.1) and the expansion of temporal operators U and R: φUψ=ψ∨(φ∧X(φUψ)) φRψ=ψ∧(φ∨X(φRψ)) 1Literal: A proposition or its negation. 33 This decomposition will define the temporal interpretations that satisfy ϕby creating different paths in the automaton. Therefore, nodes will expand by applying these rules on the formulas that must hold on them in the current step of time. The information that nodes will keep is the following: •Id: A unique node identifier. •Incoming: A set of identifiers of all the nodes that have an edge pointing to the current node. •New: A set of LTL formulae that must be satisfied immediately but that have not yet been processed (proven to hold). This set is used during the construction and is empty for all nodes of the final TGBA. •Old: A set of literals that must be satisfied immediately and have already been processed. •Next: A set of LTL formulae that must be satisfied in all successor nodes. •Untils: Bitmap of size equal to the number of U subformulas in the formula being translated. A bit is set if the corresponding subformula has been processed in this node. •Right-of-untils: A bitmap that records, for each subformula φUψ, whether ψhas been processed in this node. Furthermore, states of the TGBA will hold the following information: •Id: A state identifier. •Transitions: A set containing the incoming transitions. •Next: A set of LTL formulae that must hold in all the immediate successors of the state. And transitions will keep the following records: •Source: A set of Ids of the source states. These have a transition to the same state with the same transition label. •Label: The set of literals that must hold for the transition to be triggered. •Accepting: A bitmap that records to which accepting sets the transition belongs. Thus, New will only be used to expand a node until nodes where all formulae have been processed are reached. These nodes will represent transitions of the TGBA labeled with the formulas in their Old field. Furthermore, they will define the states where any temporal interpretation starting from them satisfies formulae in their Next set. Algorithm 4.3 shows how node expansion is performed. The line numbers in the following description refer to that algorithm. As can be seen, there are two possible cases: 34 •There are no formulas left to process (lines 2 to 12): Which implies that New is empty. In this case, if the node is equivalent to an existing state of the TGBA, they will merge. This means that the state will receive all the information regarding the transition defined on the node by its Old field. So, merging allows us to generate all the different transitions that lead to the same state. Algorithm 4.1 shows how this step is performed. Algorithm 4.1 Node and state merging. Function called from a state. 1: function merge(Node n) 2: acc =∼(n.Untils)|(n.Right-of-Untils) 3: if ∃t  Transitions s.t. (t.Label =n.Old) and (t.Accepting =acc)then 4: t.Source ∪ {n.Incoming} 5: else 6: Transitions =Transitions ∪ {new Transition nt with nt.Source =n.Incoming, 7: nt.Label =n.Old,nt.Accepting =acc} On the other hand, if the node is not equivalent to any state, a new state and transition will be created from its Next and Old fields, respectively. Moreover, a new node will be created in order to process the formulas in the Next field. •There are formulas left to process (lines 14 to 33): Formulas are processed one by one, and if no contradictions or redundancies are found, the node is expanded according to the rules. Both the test for contradiction and redundancy check are based on the ideas of [13,27]. Therefore, fields Old and Next of the current node are searched in order to find possible conflicts or redundancies. Example 3. Let ϕ=φUψbe a formula being processed by a node nduring its expansion. A contradiction would be found if ¬ϕ=¬φR¬ψhad already been processed in the node, meaning that either ¬ψbelongs to n.Old and (¬φR¬ψ) belongs to n.Next, or ¬φand ¬ψ belong to n.Old. Furthermore, the formula would be redundant if either φbelonged to n.Old and (φUψ) belonged to n.Next, or ψbelonged to n.Old. Fields Right-of-Untils and Untils are updated as necessary (lines 15-17 and 22-24) in order to keep track of the accepting sets to which the node belongs. Further explanation is provided below in this section. Once the formula is checked against contradictions and redundancies, the node is either split or updated, depending on the type of formula that is being processed. Therefore, if the formula is either a U, R or ∨formula (lines 25 to 27), the node will be split in order to create different paths that can satisfy the formula. This task is performed as shown in Figure 4.1, and it is based in the decomposition provided in Table 4.1. 35 Algorithm 4.2 Node splitting. Function called from a node. 1: function split(Formula f) 2: Create new node node2with new Id s.t. 3: (node2.Incoming =Incoming,node2.New =New ∪(New2(f) \Old), 4: node2.Old =Old ∪ {f},node2.Next =Next,node2.Untils =Untils and 5: node2.Right-of-Untils =Right-of-Untils) 6: Modify this (current node) as follows: 7: New =New ∪(New1(f) \Old), Old =Old ∪ {f},Next =Next ∪Next1(f) 8: return node2 Formula New1 Next1 New2 ϕUψ{ϕ} {φUψ} {ψ} φRψ{ψ, ϕ} {ψ, φ} {φRψ} φ∨ψ{φ} ∅ {ψ} φ∧ψ{ψ, φ} ∅ ∅ Table 4.1: Definition of New and Next for non-literals Example 4. Consider the formula φUψbeing processed in a node. Figure 4.1 shows how during its expansion, the node is split in two different nodes. The new nodes will also expand until their New set is empty. Incoming ={0} New ={φUψ} Old =∅ Next =∅ Incoming ={0} New ={ψ} Old =∅ Next =∅ Incoming ={0} New ={φ} Old =∅ Next ={φUψ} Figure 4.1: Node splitting On the other hand, if the formula is of the type φ∧ψ(lines 28 to 30) the node will not split, since φand ψneed to hold at the same time. Finally, if the formula is a literal (lines 32 to 33) it can be directly added to the Old set, since it has already been checked against contradictions and redundancies, . Accepting sets In the end, the TGBA will represent all the possible models of ϕ. Nevertheless, by construction there will be paths where φsubformulae for φUψis satisfied, but no node satisfies ψalong the path. Such paths are not models of φUψ, which requires ψto be true eventually. 36 Therefore, given that for the rest of operators any infinite path in the TGBA would be accepting, an acceptance family is defined over U subformulae. This will allow us to discard those paths that do not represent models of Uformulas. Hence, every different U subformula will define an acceptance set. These acceptance conditions will be applied to nodes during the construction (lines 6 to 8), and finally defined over TGBA transitions when merging nodes and states (see Algorithm 4.1). A node will belong to an accepting set if either the Uformula that defines that set does not hold in that node, or the right side of the formula holds. Formally, given a node n, the acceptance condition over a U formula is defined as: (φUψ processed in n)→(ψ processed in n), which is equivalent to ¬(φUψ processed in n)∨(ψ processed in n). Fields Untils and Right-of-untils are used in order to keep track of the Uformulas being processed in a node and their right subformulas, respectively. So, in order to obtain the accepting sets to which a node belongs, the acceptance condition stated above has to be applied for all the U formulas represented in the bitmaps. This can be done by carrying out the following bitwise operation: ∼(Untils)|(Right-of-Untils) Where ∼represents bitwise negation and |represents bitwise or. Example 5. Let p,qand rbe propositions and ϕ=pU(qUr). There will be an accepting set defined for ϕand another one for qUr. Therefore, n.Untils and n.Right-of-untils will have size equal to 2 for all nodes and initially, all of their bits will be set to 0. Each position of the bitmaps will reference the accepting set associated to that index, so every time one node processes ϕ, the bit 0 of n.Untils will be set to 1, and bit 1 will remain the same. The same applies to n.Right-of-untils when the right side of one of the Usubformulas is processed. Once the TGBA has been built, a degeneralization process will be applied in order to assure that all the accepting conditions are met. The result will be a Büchi automaton which represents ϕ. 37 This formula represents a logic program, and holds atoms over integer linear arithmetic. The Büchi automaton generated from ϕhas 34 states and 55 transitions, and after running the emptiness test on it, we could confirm that ϕis satisfiable. For other formulas of this magnitude we were not able to generate a Büchi automaton, since the algorithm did not provide a result in a reasonable amount of time (four hours) according to [24]. Recall that the size of the corresponding Büchi automaton can be exponential with respect to the size of the LTL formula. All formulas provided in this section were generated within seconds, but for formulas with many nested temporal operators (specially R operators), the execution time of the algorithm and the size of Büchi automata dramatically grew. One example of this fact is formula 20 from Table 4.2. Even though it is much smaller in size than ϕ, the Büchi automaton generated is significantly bigger, due to the fact that formula 20 has many nested R operators (recall that ¬(ψUφ) = ¬ψR¬φ)). 44 Chapter 5 Verification of LTL properties of computing systems In this section we provide an overview on the verification of properties of computing systems. The inherent complexity of sequential and specially concurrent computing systems makes it unfeasible to deal with them directly. Therefore, such systems are generally modeled using abstractions that build much simpler representations, while keeping the particular aspects of interest of the system. As introduced in Section 3.3, transition systems and Büchi automata can model complex systems. These provide a useful abstraction, which allows reasoning about the systems they model by only focusing in the parts of interest. Therefore, given a computing system represented by either a Büchi automaton or a transition system, and an LTL formula, it is possible to adapt the model checking method for finite-state systems described in Section 1.3 to infinite-state systems. Recall that model checking methods determine whether a system model Msatisfies a given LTL property ϕof the system. If M|=ϕ, the model checking algorithm returns a positive answer. Otherwise, a system execution path that violates ϕis returned as a counterexample. In order to determine whether M|=ϕ, it is necessary to ensure that all the executions of M satisfy ϕ. As previously stated, Mwill be either a Büchi automaton or a transition system, so it will define a language L(M)with the executions of the system it accepts. Moreover, ϕcan be represented with a Büchi automaton, so it will also define a language L(ϕ)with the executions of the system that have a correct behavior. Hence, verifying that Msatisfies ϕis reduced to checking whether: L(M)⊆L(ϕ) To this end, another approach can be followed in order to check the language inclusion. Such approach is based on the use of L(¬ϕ)rather than L(ϕ), and takes advantage of the fact that: L(M)⊆L(ϕ)↔L(M)∩L(¬ϕ) = ∅ 45 Figure 5.1: Model checking outline Hence, model checking of ϕon Mcan be performed by first negating ϕ, then building a Büchi automaton B¬ϕfrom the latter and finally carrying out the intersection between Mand B¬ϕand checking the emptiness of language defined by the result of the intersection. Figure 5.1 shows a diagram with the steps of the model checking process. Note that the output of the model checker will be either a ’Yes’ or a ’No’ along with a counterexample. Such counterexample will be helpful when estimating the possible causes of the violation of the property checked. For infinite-state systems however, there is a variation in the last step of the process, since the described emptiness test cannot be applied. Given that infinite-state systems do not provide an explicit representation of the system, the emptiness test on the intersection result would not give correct results, since concatenations of several transitions might not be feasible. Thus, other methods need to be used. Further information will be provided in the following sections, which describe the steps followed to carry out the verification of properties of infinite-state computing systems. 5.1 Büchi Automaton intersection The natural way to intersect two automatons A1and A2is to construct an automaton Awhose state space is the cross product of the state spaces of A1and A2, and let both automatons process the input simultaneously in order to create the transitions of A. For finite words, the input is accepted if each copy can generate a run which reaches an accepting state at the end of the word. For infinite words it is not that straight forward, since the acceptance condition defined over Büchi automata requires visiting accepting states infinitely often. Therefore, there is no guarantee that runs on A1and A2will ever visit accepting states simultaneously, as seen in [35]. Example 1. Consider automatons A1and A2representing languages L1= (a+ba)wand L2= (a∗ba)w, respectively. Figure 5.2 shows such automatons and Figure 5.3 shows its intersection as regular automata. As can be seen, state 11 is never reached, which leads to an incorrect behavior, since states 1are infinitely often visited in A1and A2, and Ashould reflect that. 46 0start 1 a a b 0start 1 a b a Figure 5.2: Büchi automaton A1(left) and A2(right) 00start 10 01 11 a b b a Figure 5.3: Büchi automaton Arepresenting A1∩A2(regular intersection) Therefore, in order to obtain an automaton that accepts runs accepted by both A1and A2, it is necessary to follow a different approach. Such approach will start by letting A1process the input until it reaches an accepting state. After that, it will focus the execution on A2until it reaches an accepting state, and if it does, it will change the focus to A1again, and so on. So, in order to visit infinitely often an accepting state in A2, it must visit infinitely often some accepting state also in A1and viceversa. This will make sure that the resulting automaton accepts infinite runs accepted by both A1and A2. Formally, let A1=< Q1,Σ,δ1,I1,F1>and A2=< Q2,Σ,δ2,I2,F2>, then A=A1∩A2= < Q,Σ,δ,F >, where: Q=Q1×Q2× {1,2} I=I1×I2× {1,2} F=F1×Q2× {1} Given states s1,s0 1from A1and states s2,s0 2from A2, transitions in Aare defined as follows: < s1, s2,1>a −−−−→ < s0 1, s0 2,1>iff s1 a −−−−→ s0 1and s2 a −−−−→ s0 2and s16 F1 < s1, s2,1>a −−−−→ < s0 1, s0 2,2>iff s1 a −−−−→ s0 1and s2 a −−−−→ s0 2and s1 F1 < s1, s2,2>a −−−−→ < s0 1, s0 2,2>iff s1 a −−−−→ s0 1and s2 a −−−−→ s0 2and s16 F2 < s1, s2,2>a −−−−→ < s0 1, s0 2,1>iff s1 a −−−−→ s0 1and s2 a −−−−→ s0 2and s1 F2 Example 2. Following Example 1, the correct Büchi automaton representing the intersection between A1and A2is shown in Figure 5.4. Unreachable states are left for better understanding of the result. 47 00_1 start 10_1 10_2 00_2 01_1 01_211_1 11_2 a a a b a a aa Figure 5.4: Büchi automaton Arepresenting A1∩A2 Once the intersection has been defined for arbitrary automatons, we introduce the special case of either F1=Q1or F2=Q2(i.e. one of the automatons only has accepting states). In this case, we only need to make sure that the resulting automaton accepts infinite runs accepted by the automaton which has some non-accepting states. Intuitively, if an automaton only has accepting states, it will accept any infinite run. Therefore, when intersecting such automaton with an arbitrary one, the former will restrict the acceptance condition of the resulting automaton. Thus, if F2=Q2for example, we will have: Q=Q1×Q2 I=I1×I2 F=F1×Q2 And transitions will be defined such that given states s1,s0 1from A1and states s2,s0 2from A2: < s1, s2>a −−−−→ < s0 1, s0 2>iff s1 a −−−−→ s0 1and s2 a −−−−→ s0 2 Example 3. Following Example 1, consider A0 2is A2with only accepting states. Figure 5.5 shows how the intersection between A1and A0 2would be in that case. 00start 10 01 11 a b b a Figure 5.5: Büchi automaton Arepresenting A1∩A0 2 For the intersection of a transition system with a Büchi automaton, the same approach is followed, but transitions of the final model will have the assignments found in the transitions of the transition 48 system that were combined with those of the Büchi automaton. Therefore, the final result will be neither a Büchi automaton nor a transition system, but a combination of both. Example 4. Consider the computing system represented by the program shown below, and the LTL property ϕ= (j > i)U(j=i), which we want to verify on the system. The negation of the LTL property is ¬ϕ=(¬(j > i)R¬(j=i)). Figure 5.6 shows the Büchi automaton for ¬ϕ, and Figures 5.7 and 5.8 show the transition systems for the program and the intersection between such transition system and the Büchi automaton, respectively. The results shown were obtained with the use of our tools. int main() { int a; int n,m; assume(n<=m); int j=m; int i=0; ltl_property((j > i) U (j = i)); while (j>=0){ j--; i++; } } Figure 5.6: Computing system (left) and Büchi automaton for the formula (j > i)U(j=i) (right) As can be seen in Figure 5.8, the resulting transition system has transitions holding both conditions and assignments, and some of its states are accepting. This transition system represents all the executions of the program that satisfy ¬ϕ, if any. 49 Figure 5.7: Transition system for the program 50 Figure 5.8: Intersection between transition system and Büchi automaton Finally, once the intersection is performed, it will be necessary to check whether the result determines that the system verifies the property or not. 5.2 Verification We aim to verify LTL properties on infinite state systems, hence the methods that we will use do not rely on an explicit representation of the state space. Rather than that, we will exploit the expressive power transition systems. The use of such representations implies that methods previously described for the emptiness check 51 (see Section 4.3) cannot be applied, since they could lead to unfeasible accepting traces. Example 1. Consider the transition system in Figure 5.9 obtained from the program shown. If we considered location l1as an accepting state, the Nested DFS algorithm would determine that there always exists an infinite execution that can go through l1infinitely often (i.e. an accepting trace). Nevertheless, it can be seen that for instance, with values x < 0and y≥1, there are no infinite traces and, in fact, this transition system does not have any infinite run. int main() { int x=undet(),y=undet(),z=undet(); l1: while (y>=1) { x--; l2: while (y<z) { x++; z--; } y=x+y; } } Figure 5.9: Transition System example Therefore, instead of performing the emptiness test, one possible adaptation for infinite-state systems could be to use methods based on the notion of program termination [23,36], which will allow us to find feasible infinite traces in the model. However, the application of such methods is out of the scope of this project, since we aimed to provide a result from which a program analysis tool such as V eryMax could yield a final result . 52 Chapter 6 Conclusions We have developed tools which allow us to check LTL satisfiability of formulas coming from logic programs. Moreover, our tools also provide models which can be fed to program analysis methods in order to check the satisfiability of LTL properties on infinite-state systems. Therefore, our implementation provides models for LTL formulas in the shape of Büchi automata, and allows the combination of such automatons with models representing computing systems. The satisfiability check for logic programs is performed by analyzing the Büchi automatons obtained from the formulas representing them. This method yields good results when dealing with small formulas, but becomes impractical as the sizes of the formulas increase. The same applies to the Büchi automatons obtained from the combination of a system model and the Büchi automaton representing an LTL property. Since combining the models means performing an automaton intersection, the size of the result dramatically increases as the models grow. Hence, our tools efficiently generate models for many LTL formulas used in practice. However, further research should be made in order to find methods that optimize the generation of Büchi automata, thereby making some larger LTL formulas treatable. 53