Structured Object-Oriented Formal Language and Method: 7th International Workshop, SOFL+MSVL 2017, Xi'an, China, November 16, 2017, Revised Selected ... Computer Science and General Issues)

Preface
Organization
Contents
Animation and Prototyping
Graphically Perceiving Characteristics of the MCS Lock and Model Checking Them
	1 Introduction
	2 Preliminaries
	3 MCS List-Based Queuing Lock
	4 Maude
	5 Analysis of MCS Protocol
		5.1 Invariant Model Checking with Search
		5.2 Graphical Animations of MCS Protocol
		5.3 Perceiving Characteristics with Graphical Animations
		5.4 Confirming Characteristics with Maude
		5.5 LTL Model Checking
		5.6 A Naive Way to Disuse comp&swap
		5.7 The Mellor-Crummey and Scott\'s Way to Disuse comp&swap
	6 Related Work
	7 Conclusion
	References
An Investigation of Integrating a GUI-Aided Approach and a Specification-Based Testing
	1 Introduction
	2 A GUI-Aided Approach
	3 Specification-Based Testing
		3.1 Test Strategy
		3.2 Test Conditions
		3.3 Test Cases and Evaluation of the Test Results
	4 Discussions
	5 Conclusions
	References
Graph Theory
On the Cooperative Graph Searching Problem
	1 Introduction
	2 Preliminary Results
	3 NP-Completeness Result
	4 Polynomial-Time Algorithm for Grid Graphs
	5 Conclusion
	References
Model Checking
Boosting UPPAAL for OSEK/VDX Applications with a Sequentialization Approach
	1 Introduction
	2 Background of OSEK/VDX
		2.1 OSEK/VDX OS
		2.2 Running Application
	3 The Existing Method for OSEK/VDX Applications
		3.1 Non-deterministic and Deterministic Schedulers
		3.2 Application Model in UPPAAL
		3.3 Advantages and Disadvantages of the Existing Method
	4 Our Approach for Boosting UPPAAL
		4.1 Key Idea of Our Approach
		4.2 Sequential Translation
		4.3 Example
		4.4 Advantages and Disadvantages of Our Approach
	5 Experiments and Discussion
		5.1 Experiments
		5.2 Discussion
	6 Related Work
	7 Conclusion and Future Work
	References
The Complexity of Linear-Time Temporal Logic Model Repair
	1 Introduction
	2 Preliminaries
		2.1 Kripke Structure
		2.2 Linear-Time Temporal Logic
		2.3 LTL Model Checking
	3 Model Repair of LTL with States
		3.1 Modified LTL Graph
		3.2 Complexity of LTL Model Repair with States
	4 Hardness of Decision Version
	5 Model Repair with Transition Relations
	6 Examples
		6.1 MinMax Example
		6.2 Concurrent Program Example
	7 Conclusion
	References
Extending UML for Model Checking
	1 Introduction
	2 Preliminaries
		2.1 Unified Modeling Language
		2.2 Modeling, Simulation and Verification Language
	3 Structures of xUML4MC
		3.1 Fundamental Notations
		3.2 Visual Notations
		3.3 System Modeling with xUML4MC
	4 Translation of xUML4MC Model into MSVL Model
		4.1 Formal Definition of xUML4MC Model
		4.2 Conversion from xUML4MC Model to Abstract Syntax Tree
		4.3 Conversion from AST to MSVL
		4.4 Translation Example
	5 Related Works
	6 Conclusion
	References
Modeling and Specification
Foundation of a Framework to Support Compliance Checking in Construction Industry
	Abstract
	1 Introduction
	2 Related Work
	3 An Illustrative Example of Compliance Checking
	4 A Framework to Support Compliance Checking
	5 Formalization of Conformance Checking
	6 Conclusion and Future Work
	Acknowledgement
	References
An Improved Reliability Testing Model Based on SOFL
	Abstract
	1 Introduction
	2 The Method of Specification Formalization with SOFL
		2.1 The Composition of SOFL Formal Specification
		2.2 The Composition of Reliability Testing Model
	3 The Improved Method of Building a Test Model
	4 Case Study of DG-CDFD
		4.1 The Steps of Building Model
		4.2 Formalize the Specification
		4.3 Modeling Process with the DG-CDFD
	5 Conclusion
	Acknowledgements
	References
A Framework Based on MSVL for Verifying Probabilistic Properties in Social Networks
	1 Introduction
	2 Preliminaries
		2.1 Hidden Markov Model
		2.2 MSVL and MSV Platform
	3 Verifying Probabilistic Properties in Social Networks
	4 Case Study
		4.1 Modeling
		4.2 Verification
	5 Related Work
	6 Conclusions
	7 Appendix: The MSVL Program
	References
Implementing MapReduce with MSVL
	1 Introduction
	2 Preliminaries
		2.1 Modeling, Simulation and Verification Language
		2.2 Cylinder Computation Model
	3 MapReduce Work Flow
	4 Principle of Programming with MSVL
		4.1 Dealing with Hardware File Systems
		4.2 Partitioning Tasks into Parallel Computation Blocks
		4.3 Constructing Data Structures
		4.4 Verifying Programs
	5 Case Study: Sparse Matrix Multiplication
		5.1 Matrix Representation
		5.2 Map and Reduce of Matrix Multiplication in the First Phase
		5.3 Map and Reduce of Matrix Multiplication in the Second Phase
	6 Conclusion
	References
Verification and Validation
A Software Tool to Support the “Vibration’’ Method
	Abstract
	1 Introduction
	2 SOFL Specification and Functional Scenario-Based Testing
	3 Introduction to V-Method
		3.1 Principle of the V-Method
		3.2 Example
	4 Supporting Tool for “Vibration” Method
		4.1 Functions
		4.2 Quality Assurance of the Tool Using SOFL
	5 Experiments
		5.1 BMI (Body Mass Index) Calculation
		5.2 Balance Ratio Calculation
		5.3 Train Fare System
		5.4 Experiment Results and Analysis
	6 Discussion
	7 Conclusion and Future Work
	Acknowledgments
	Appendix
	References
A Software Tool to Support Scenario-Based Formal Specification for Error Prevention
	Abstract
	1 Introduction
	2 Scenario-Based Formal Specification
		2.1 Process Specification
		2.2 Functional Scenarios
		2.3 Scenario-Based Formal Specification
	3 Principles
		3.1 Checking Internal Consistency
		3.2 Automatic Checking the Internal Consistency
		3.3 Automatic Translation to Tabular Form
	4 Software Tool
		4.1 Implementation Structure
		4.2 Case Study
	5 Related Work
	6 Conclusion and Future Work
	Acknowledgments
	References
A Proof Score Approach to Formal Verification of an Imperative Programming Language Compiler
	1 Introduction
	2 Formal Specification and Verification in CafeOBJ
	3 Minila
	4 Formal Verification
	5 Discussion
	6 Conclusion
	References
Author Index