Structured Object-Oriented Formal Language and Method

The MCS list-based queuing lock (MCS) is a mutual exclusion protocol whose variants have been used in Java virtual machines. MCS is specified as a state machine in Maude, a rewriting logic-based computer language and system. We have developed a tool (called SMGA) that tales a finite computation generated from a state machine and displays its graphical animations. MCS is used to describe how such graphical animations help human beings perceive characteristics of the state machine of MCS. Such characteristics can be confirmed by Maude model checking facilities. The characteristics graphically perceived and confirmed by model checking could be used as lemmas to theorem prove that MCS enjoys some desired properties. SMGA can also display graphical animations of counterexamples presented by the Maude LTL model checker.

Formal methods mainly aim to improve software reliability by systematic refinements and/or verifications between specifications and implementations in mathematical ways. However, they are not enough for validating whether the system functions meet the user’s requirements. We propose a combination of software prototyping and formal methods to address this problem. Our prototype provides desirable behaviors of system functions, and supports the generation of test cases by finding out input and output data related to the functions. This paper describes a case study for integrating a GUI-aided approach to constructing formal specifications and a testing-based verification of programs. Our research shows a demand for additional work on verifying external database accesses in automatic test case generation from formal specifications.

In this paper, we introduce a new variation of graph searching problem, namely, cooperative graph searching problem. We define that a searcher is isolated if there is no other searchers on its close neighborhood. In this variant, we add an additional constrain that every searcher would not be isolated after each searching step. Therefore, we can make sure that every searcher can be cooperated by another searcher. We prove that the cooperative graph searching problem is NP-complete on general graphs and propose polynomial-time algorithms for the problem on grid graphs.

The OSEK/VDX standard has been widely adopted by automotive manufacturers for vehicle mounted systems. The ever increasing complexity of the system has created a challenge for examining the timing properties of the developed OSEK/VDX applications in exhaustive way, such as reachability property. Model checking as an exhaustive verification technique has attracted great attentions in the automotive industry. To verify OSEK/VDX applications by using model checking, a tentative method has been proposed based on the model checker UPPAAL. However, the existing method is usually not scalable to verify a large-scale OSEK/VDX application since the constructed application model is too complex. In this paper, we propose an efficient approach to simplify the application model for making UPPAAL more scalable in verifying large-scale OSEK/VDX applications. We evaluated our approach based on a series of experiments. The experimental results show that our approach is not only capable of efficiently simplifying the OSEK/VDX application models, but also of making the model checker UPPAAL competent in dealing with the OSEK/VDX applications with industrial complexity.

We propose the model repair problem of the linear-time temporal logic. Informally, the repair problem asks for a minimum set of states in a given Kripke structure M, whose modification can make the given LTL formula satisfiable. We will examplify the application of the model and study the computational complexity of the problem. We will show the problem can be solved in exponential time but remains NP-hard even if k is a constant.

To solve the problem that UML (Unified Modeling Language) design model cannot be model-checked for its rough semantics, an extension of UML, called xUML4MC, is defined by extending the activity diagram with accurate syntax and semantics to model the activities of an object. Besides, the technique for automatical transformation of xUML4MC model into MSVL (Modeling, Simulation and Verification Language) model is also presented, which in turn can be verified with model checking tool MSV. The formalism arms the classical visual specification language UML with the power of model checking, and helps to promote the quality of software system.

Computer use is pervasive in our daily life and the increasing demand for computer applications has penetrated into various domains. Construction industry has become one of domains which are more reliable on the application of computer to implement regulatory compliance checking. Like many safety critical domains, the construction domain has its own set of international building codes on construction projects which must comply with. With the increasing complexity of construction projects, many manual compliance checking techniques have shown some serious issues. First, the manual techniques are error-prone due to human errors. Second, the complexity of a construction project exceeds the human limit to deal with. Third, the evolution of a construction project is inevitable and the human maintenance of a construction project is almost impossible because either the memory of the original project design has faked away or some development team members are gone. So, it has become a new trend to employ computers to support automatic regulatory compliance checking in construction industry. In this paper, we propose a novel framework to support compliance checking with the emphasis on the foundation of automatic regulatory compliance checking to certify whether a construction project complies with some international building codes. An example is illustrated how compliance checking is performed in the framework.

With the rapid growing size of industry software, software reliability has become a necessary factor to measure software quality. Software testing, which can quantify and assess software reliability by establishing the model of software reliability, is an important method to verify software reliability. SOFL is an object-oriented structured formal language and engineering approach. SOFL consists of Condition Data Flow Diagram (CDFD) and formal description of CDFD called Module. It makes an accurate explanation of the software function, which is the basis of reliability testing. However, the reliability testing also need to consider the frequency of functional use, which cannot be expressed by SOFL. Therefore, this paper explores an improved method named DG-CDFD. It uses the state diagram to express the probability of transfer between different states based on CDFD, and builds a reliability testing model. Finally, this paper verifies the feasibility of this method through a case model building.

In social networks, there are many phenomena related to randomness, such as interaction behaviors of users and dynamic changes of network structure. In this work, a framework based on MSVL (Modeling, Simulation and Verification Language) for verifying probabilistic properties in social networks is proposed. First, a hidden Markov model (HMM) is trained with the real social network dataset and implemented by MSVL. Then, an observed sequence is input into the trained HMM to obtain relevant information of the network, according to specialized algorithms. Next, a probabilistic property is specified with a formula of Propositional Projection Temporal Logic (PPTL). Finally, it is verified whether the MSVL model satisfies the PPTL property by model checking. An example of Sina Weibo is provided to illustrate how the framework works.

This paper presents an approach to implementing MapReduce processes with Modeling Simulation and Verification Language (MSVL). This facilitates programmers not only to deal with large data sets but also to verify properties of programs in a convenient way.

The “Vibration” method proposed in the literature offers a strategy for generating test data from an atomic predicate in a specification with the aim of achieving full path coverage in the program that implements the function defined by the predicate. However, how to efficiently generate adequate test data using the method from the same predicate to quickly traverse all of the related paths in the program is still an open problem. In this paper, we describe a prototype software tool we have built recently that supports the test data generation based on the principle of the “Vibration” method and an experiment to evaluate the effectiveness of the “Vibration” method supported by the tool.

Formal specification can be an error-prone process for complex systems and how to efficiently write correct specifications is still a challenge for practitioners in industry. This paper presents a software tool to support the scenario-based formal specification approach developed in the SOFL formal engineering method. Using the tool, the current version of the formal specification under construction can be automatically checked to ensure the internal consistency and some further contents of the specification may be automatically predicated to facilitate the user in completing the specification. To improve the readability of the formal specification, the tool can also automatically translate the textual format of the specification into a comprehensible tabular format. All of these three functions can be helpful to prevent errors during the construction of the specification. We discuss each of the functions by first presenting its principle and then illustrating it with examples. We present a case study to show how the tool supports the scenario-based specification approach. Finally, we conclude the paper and suggest topics for future research.

An interpreter for an imperative programming language called Minila has been formally specified in CafeOBJ, an executable specification language, and so have a virtually machine (VM) and a compiler. The compiler transforms a Minila program into an instruction sequence processed by the VM. Since the formal specifications are executable, it is doable to test if for any concrete terminating program p the result of interpreting p is the same as the one of processing by the VM the instruction sequence generated from p by the compiler, where the result is an environment, a variable-value pair collection. The equivalence is called the Minila compiler correctness with respect to p. In addition to test, properties of CafeOBJ specifications can be theorem proved by writing what are called proof scores in CafeOBJ and executing them with CafeOBJ. The Minila compiler correctness for all terminating programs in Minila has been theorem proved.