CSE 450/598 Project1
Software Verification in Software Engineering:
The Analysis of a Linear Temporal Logic
To Buchi Automata Algorithm
Group P - 204
Matthew Warren
Naveen.Tummala
Swami.Venkataramani
Ranjit Singh
CSE 450/598
Department of Computer Science & Engineering
Arizona State University
Introduction
1.0 What is Software Engineering?
1.1 General View of Software Engineering
1.2 The generalized Software Engineering process in depth
1.3 Section Summary
2.0 A Discussion on Related Languages and Tools
2.1 Message Sequence Charts [10]
2.2 Live Sequence Charts [17]
2.3 Statemate [11]
2.4 Rhapsody
2.5 XUML
2.6 Symbolic model verifier (SMV) [13]
2.7 SPIN [14]
2.8 INCA [15]
2.9 FLAVERS [16]
2.10 Summary
3.0 Model Checking
3.1 Linear Temporal Logic
3.2 Buchi Automata
4.0 Approach
4.1 Data Structure
4.2 Algorithm
5.0 Asymptotic Time Complexity Analysis
5.1 Analysis Preliminaries
5.2 Worst Case Analysis
5.3 Best Case Analysis
5.4 Results Discussion
6.0 Proof of Correctness
6.1 Lemma 1
6.2 Lemma 2
6.3 Lemma 3
6.4 Lemma 4
6.5 Lemma 5
6.6 Lemma 6
6.7 Lemma 7
6.8 Lemma 8
6.9 Lemma 9
7.0 Possible Improvements to the Algorithm [7]
7.1 Adding a Nextime Operator
7.2 Pure “On-the-fly” Construction
7.3 Improvements to Efficiency
8.0 Conclusion
References
Introduction
Software plays a critical role in today’s society. Because of the pervasiveness of software in vital applications, such as nuclear reactors, medical equipment and military machinery, human life literally depends on the correct and accurate implementation of software. In such applications one cannot release software simply because ‘it appears to work’, or ‘it seems accurate’. Instead a more formal and rigorous technique is required to guarantee that software meets essential requirements.
The concept of software verification is not new and much research has been done in this domain. In particular, there is much study in the area of how formal logics can be applied in the analysis of computer programs and their design [6]. Formal logics allow for systems to be developed in which certain properties regarding the system can be proven. This paper aims to take a brief venture into the domain of formal verification within software engineering and analyzes an algorithm that aids in the formal verification process.
This paper is divided into two main parts. The first part deals with software engineering and verification in general and briefly covers the gambit of the software process and available tools. The second part focuses on model checking and an algorithm used in the software verification process. The algorithm is decomposed, explained and its worst and best case running times are analyzed and derived. Finally some proofs on the correctness of the algorithm are given followed a brief conclusion of the findings.
PART I
1.0 What is Software Engineering?
If science is the search for the fundamental principles that govern the world around us and explain the phenomena we see, then a case can be made that Software Engineering is the “science” underlying the field of software development. Software engineering is a very eloquent science; it is a layered technology that is composed of many problem solving recipes and many opportunities for verifying those problem-solving recipes or algorithms. Any engineering approach (including software engineering) must rest on an organizational commitment to quality. Total quality management and similar philosophies foster a continuous process improvement culture, and it is this culture that ultimately leads to the development of increasingly more mature approaches to software engineering. The bedrock that supports software engineering is a quality focus.
The foundation for software engineering, as Roger Pressman [18] brought to light, is the process layer. Software engineering process is the glue that holds the technology layers together and enables rational and timely development of computer software. Furthermore, this research paper is conducted in order to explore methods of the engineering process that can be automated in the area of verification, so that the correctness of algorithms can be more readily verified than before. In other words, as Dimitra Giannakopoulou and Flavio Lerda introduced in [4] how, by labeling automata transitions rather than states, we significantly reduce the size of automata generated by existing tableau-based translation algorithms. However, it also involves it's own algorithmic issues and is not nearly as well researched. The mere idea of fashioning an algorithm to verify the eminence of software is considered a science-fiction-like feat.
Fashioning software engineering methods provide the technical "how to's" for building software. Methods encompass a broad array of tasks that include requirements analysis, design, program construction, testing, and maintenance. Software engineering methods rely on a set of basic principles that govern each area of the technology and include modeling activities and other descriptive techniques.
Software engineering tools provide automated or semi-automated support for methods. When tools are integrated so that information created by one tool can be used by another, a system for the support of software development, called computer-aided software engineering (CASE), is established. As pointed out in [5], CASE tools have recently evolved into more advanced assistants to the software engineering verification methods introduced above. Such CASE tools include SPIN (which actually proves the correctness of process interactions), Executable UML (XUML), Architectural Development Languages (ADL), Statemate and Rhapsody, and Rose RealTime (These tools are discussed further in section 2).
1.1 General View of Software Engineering
Engineering, in general, is the analysis, design, construction, verification, and management of technical (or social) entities. Regardless of the entity to be engineered, the following questions must be asked and answered:
- What is the problem to be solved?
- What characteristics of the entity are used to solve the problem?
- How will the entity (and the solution) be realized?
- How will be entity be constructed?
- What approach will be used to uncover defects that were made in the design and construction of the entity?
- How will the entity be supported over the long term when users of the entity request corrections, adaptations, and enhancements?
Software Engineering is the engineering of software (program, associated documentation, and data) entities, and the work associated with software engineering can be categorized into three generic phases, regardless of application area, project size, or complexity [18]. Each phase addresses one or more of the questions noted previously. The three phases: definition, development, and maintenance, are encountered in all software development, regardless of application area, project size, or complexity.
The definition phase, by far, is the most crucial phase in successful and maintenance-free-production, focusing on what the customer wants. That is, during definition, the software developer attempts to identify:
- What information is to be processed
- What functionality and performance requirements are desired
- What interfaces are to be established
- What design constraints exist
- How data structures and software architectures are to be designed:
- How procedural details are to be implemented
- What validation criteria are required to define a successful system
Thus the key requirements of the system and the software are identified.
The development phase focuses on how the software is constructed. That is, during development, the software developer attempts to describe how the design will be translated into a programming language, and how testing will be performed.
The maintenance phase focuses on change that is associated with error correction, increasing the overall quality of the software developed, adaptations required as the software's environment evolves, and modifications due to enhancements brought about by changing customer requirements. The maintenance phase reapplies the steps of the definition and development phases, but does so in the context of existing software.
1.2 The generalized Software Engineering process in depth
To solve actual problems in an industry setting, a software engineer or a team of engineers must incorporate a development strategy that encompasses the process, methods, tools and generic phases [18]. This strategy is often referred to as a process model. A process model for software engineering is chosen based on the nature of the project and application, the methods and tools to be used, and the controls and deliverables that are required.
All software development can be characterized as a problem-solving loop in which four distinct stages are encountered: status quo, problem definition, technical development and solution integration. Status quo represents the current state of affairs; problem definition identifies the specific problem to be solved; technical development solves the problem through the application of some technology, and solution integration delivers the results to those who requested the solution in the first place.
This problem-solving loop applies to software engineering work at many different levels of resolution. It can be used at the macro level when the entire application is considered, at a mid-level when program components are being engineered, and even at the line of code level. Therefore, a fractal representation can be used to provide an idealized view of process.
Figure 1 - Illustration of the breakdown of stages in the problem-solving loop
As shown in figure 1, each stage in the problem-solving loop contains an identical problem-solving loop, which contains still another problem solving loop (in the same manner as a divide and conquer algorithm divides its domain to a final conquering stage) [19].
Because of this standard problem-solving loop arrangement, many models have been built to represent the different strategies available, in the development of software. While a variety of different process models exist, the point of this paper is not to familiarize the reader with all generality of software engineering process models. Rather this section of the document is intended to set the stage for the reader to denote the importance of the various stages of software development, more specifically the design to implementation stage.
With that being said, the classic life cycle process model is one that eloquently animates the transition from design to code generation (implementation) and the importance of verifying the safety and quality of the implemented software. The classic life cycle suggests a systematic, sequential approach to software development that begins at the system level and progresses through analysis, design, coding, testing, and support. Figure 2 illustrates the classic life cycle model for software engineering.
Figure 2 - Image of the classic life cycle model for software engineering
Modeled after a conventional engineering cycle, the classic life cycle model encompasses the following activities:
System modeling = Because software is usually part of a larger system, work begins by establishing requirements for all system elements and then allocating some subset of these requirements to software. This system view is essential when software must interface with other elements such as hardware, people and databases. System engineering and analysis encompasses requirements gathering at the system level with a small amount of top-level design and analysis.
Software requirements analysis = The requirements gathering process is intensified and focused specifically on software. To understand the nature of the program(s) to be built, the software engineer (“analyst”) must understand the information domain for the software, as well as required function, behavior, performance, and interface. Requirements for both the system and the software are documented and reviewed with the customer [18].
Design = Software design is actually a multi-step process that focuses on four distinct attributes of the program: data structure, software architecture, procedural detail and interface characterization. The design process translates requirements into a representation of the software that can be assessed for quality before coding begins. Like requirements, the design is documented and becomes part of the software configuration.
Code generation = The design must be translated into a machine-readable form. The code generation step performs this task. If design is performed in a detailed manner, code generation can be accomplished mechanistically.
Testing = Once code has been generated, program testing begins. The testing process focuses on the logical internals of the software, ensuring that all statements have been tested, and on the functional externals that is, conducting tests to uncover errors and ensure that defined input will produce actual results that agree with required results.
Maintenance/Support = Software will undoubtedly undergo change after it is delivered to the customer (possible exception is embedded software). Change will occur because errors have been encountered, because software must be adapted to accommodate changes in its external environment (e.g. a change required because of a new operating system or peripheral device), or because the customer requires functional or performance enhancements [18]. Software maintenance typically reapplies each of the preceding life-cycle steps to an existing program rather than a new one.
1.3 Section Summary
While real projects rarely follow the classic life cycle flow that the model proposes, the point of this example is to make apparent to the reader the importance of absolute verification of the requirements and hence safety of the customer, by assuring the impeccable quality of the software through LTL to Buchi modeling. Verifying this particular aspect of the model (or any existing development model for that matter) will ensure full requirements representation in the deliverable. Further improvements of this process may provide more time for other phases of the process. Subsequently, if more time can be spent on the analysis of the criticality of the application, as well as a more intense design phase to support the intentions of the customer to the exact bit, the quality assurance of the software would be theoretically flawless.
2.0 A Discussion on Related Languages and Tools
As mentioned in the previous section, software development has been a well-researched topic and there are sophisticated tools developed at different stages of the software development, such that at one point verification has become the bottleneck of complexity of software development. Various formal verification techniques and tools have come to the rescue of this software bottleneck. Current verification techniques use mathematical methods to quickly verify the system against the model instead of applying a set of elaborate tests. The broad classification of the software development languages is given in figure 3.
Figure 3
Before we discuss some of the verification techniques, we present some of the tools and techniques used at various levels of software development. Over the years, the main approach to develop a system model has been structured-analysis and design (SA/SD) and object-oriented analysis and design (OOAD)[9]. The basic SA/SD is based on raising classical programming concepts to system modeling. These models are based on functional decomposition and information flow and depicted by flow diagrams. The enhanced SA/SD uses state diagrams or state charts. Later, State mate was released which is a tool that enables model-execution and code generation.
With the same motive (as SA/SD) of raising the programming concepts to system modeling, OOAD recommended various forms of class and object diagrams for modeling system structure. The links between behavior and structure should be defined in sufficient detail in order to support the construction of tools that enable model execution and full code generation. Some of the tools which are able to do this are Object time (based on rational real-time), Rhapsody. The class/object diagrams and the state charts included in UML is called xUML (executable UML). xUML is a part of UML that specifies unambiguous, executable and therefore implementable models.
Method checking, equivalence checking are different methods of model verification. Currently, there are a wide variety of model verification tools. Some tools are designed and used for verification of software systems or communication protocols and some are used for verification of hardware systems. Most of these tools allow several forms of specification, including the temporal logics CTL and LTL, finite automata and refinement specifications. They also include an easy-to-use graphical user interface and source level debugging capabilities. Some of the tools for model checking are SMV, SPIN, INCA and FLAVERS. The performance of these tools varies significantly on the type of problem and its properties. Some of the above mentioned tools and techniques will be discussed in detail in the subsections.
2.1 Message Sequence Charts [10]
Message sequence charts (MSCs) are used in the design phase of a distributed system to record intended system behaviors. Message sequence charts (MSCs) are a standardized formalism for the specification of the system’s communication behavior that is widely used by industry for system integration and acceptance testing.
Message sequence charts (MSCs), also known as time sequence diagrams, message flow diagrams, or object interaction diagrams are a popular visual formalism for documenting design requirements for concurrent systems. MSCs are often used in the first attempts to formalize design requirements for a new system and the protocols it supports. MSCs represent typical execution scenarios, providing examples of either normal or exceptional executions of the proposed system.
The strength of the message sequence charts lies in their ability to describe communication between cooperating processes. Consider an example shown in figure 4.
Figure 4
The example above shows a single process. The rectangle contains the process identifier (counter in this example). The lifeline of the process extends downwards. The arrows represent the messages passed from the sending to the receiving processes.
However MSCs suffer from two major short comings: 1) they do not allow message abstraction and 2) they do not explicitly mention the status of each scenario (unsure of whether it is an example or universal rule). So live sequence charts (LSCs) are a formidable candidate for overcoming such shortcomings.