Structured Object-Oriented Formal Language and Method

1. Front Matter

   Pages I-VIII

   PDF

2. Modeling and Specification

   1. Front Matter

      Pages 1-1

      PDF

   2. Genericity in PAR Platform

      • Jinyun Xue

      Pages 3-14

   3. Modeling and Verification of an Interrupt System in \(\mu \)C/OS-III with TMSVL

      • Jin Cui, Zhenhua Duan, Cong Tian, Nan Zhang

      Pages 15-28

   4. The Interchange Format of Tabular Expressions Using XML

      • Mao Huang, Yihai Chen, Ridha Khedri, Huaikou Miao

      Pages 29-43

   5. A GUI-Aided Approach to Formal Specification Construction

      • Shaoying Liu

      Pages 44-56

3. Testing and Debugging

   1. Front Matter

      Pages 57-57

      PDF

   2. Automatic Generation of Specification-Based Test Cases by Applying Genetic Algorithms in Reinforcement Learning

      • Yuji Sato, Taku Sugihara

      Pages 59-71

   3. Fault Localization of Timed Automata Using Maximum Satisfiability

      • Shin Nakajima, Si-Mohamed Lamraoui

      Pages 72-85

   4. Automated Program Debugging for Multiple Bugs Based on Semantic Analysis

      • Aishan Liu, Li Li, Jie Luo

      Pages 86-100

4. Model Checking and Verification

   1. Front Matter

      Pages 101-101

      PDF

   2. Model Checking Process Scheduling over Multi-core Computer System with MSVL

      • Xinfeng Shu, Zhenhua Duan

      Pages 103-117

   3. A Method Based on MSVL for Verification of the Social Network Privacy Policy

      • Xiaobing Wang, Tao Sun

      Pages 118-131

   4. A Case Study: SOFL + Model Checking for OSEK/VDX Application

      • Zhuo Cheng, Haitao Zhang, Yasuo Tan, Yuto Lim

      Pages 132-146

   5. On Reachability Analysis of Updatable Timed Automata with One Updatable Clock

      • Yunqing Wen, Guoqiang Li, Shoji Yuen

      Pages 147-161

5. Algorithm and Transformation

   1. Front Matter

      Pages 163-163

      PDF

   2. Research on Formal Development of Non-recursive Algorithms of Graph Search

      • Qimin Hu, Jinyun Xue, Zhen You

      Pages 165-178

   3. LtlNfBa: Making LTL Translation More Practical

      • Cong Tian, Jun Song, Zhenhua Duan, Zhao Duan

      Pages 179-194

   4. PPTL_SPIN: A SPIN Based Model Checker for Propositional Projection Temporal Logic

      • Xiaoming Zhang, Zhenhua Duan, Cong Tian

      Pages 195-205

   5. Automatic Transformation from SOFL Module Specifications to Program Structures

      • Xiongwen Luo, Shaoying Liu

      Pages 206-218

This book constitutes the thoroughly refereed post-workshop proceedings of the 5th International Workshop on Structured Object-Oriented Formal Language and Method, SOFL+MSVL 2015, held in Paris, France, in November 2015. The 15 papers presented in this volume were carefully reviewed and selected from 22 submissions. The focus of this workshops was on following subjects: Modeling, specification, verification, model checking, testing, debugging, transformation, and algorithm.

• Generic programming
• Genetic algorithm
• Model checking
• Reinforcement learning
• Semantic analysis
• Automated debugging
• Formal development
• Formal semantics
• Linear temporal logic
• Model driven
• Process scheduling
• Real-time systems
• Social networks
• Software analysis
• Software engineering
• Specification
• System modeling
• Temporal logic
• Verification
• XML

• Hosei University, Koganei-shi, Japan

  Shaoying Liu

• Xidian University, Xi’an, China

  Zhenhua Duan

Policies and ethics