Skip to main content

Über dieses Buch

This book constitutes the thoroughly refereed workshop proceedings of the 7th International Workshop on Structured Object-Oriented Formal Language and Method, SOFL+MSVL 2017, held in Xi’an, China, in November 2017.

The 13 revised full papers included in the volume were carefully reviewed and selected from 21 submissions. They are organized in the following topical sections: animation and prototyping; graph theory; model checking; modeling and specification; and verification and validation.



Animation and Prototyping


Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them

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.
Tam Thi Thanh Nguyen, Kazuhiro Ogata

An Investigation of Integrating a GUI-Aided Approach and a Specification-Based Testing

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.
Fumiko Nagoya, Shaoying Liu

Graph Theory


On the Cooperative Graph Searching Problem

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.
Chin-Fu Lin, Ondřej Navrátil, Sheng-Lung Peng

Model Checking


Boosting Uppaal for OSEK/VDX Applications with a Sequentialization Approach

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.
Haitao Zhang, Zhuo Cheng, Jianxin Xue, Yonggang Lu

The Complexity of Linear-Time Temporal Logic Model Repair

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.
Xiuting Tao, Guoqiang Li

Extending UML for Model Checking

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.
Xinfeng Shu, Mengnan Wang, Xiaobing Wang

Modeling and Specification


Foundation of a Framework to Support Compliance Checking in Construction Industry

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.
Wuwei Shen, Guangyuan Li, Chung-Ling Lin, Hongliang Liang

An Improved Reliability Testing Model Based on SOFL

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.
Zhouxian Jiang, Honghui Li, Xuetao Tian

A Framework Based on MSVL for Verifying Probabilistic Properties in Social Networks

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.
Xiaobing Wang, Liyuan Ren, Liang Zhao, Xinfeng Shu

Implementing MapReduce with MSVL

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.
Nan Zhang, Meng Wang, Zhenhua Duan, Cong Tian, Jin Cui

Verification and Validation


A Software Tool to Support the “Vibration’’ Method

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.
Pan Zhao, Shaoying Liu

A Software Tool to Support Scenario-Based Formal Specification for Error Prevention

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.
Siyuan Li, Shaoying Liu

A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler

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.
Dorian Daudier, Trinh Ngoc Quoc Bao, Kazuhiro Ogata


Weitere Informationen

Premium Partner