Structured Object-Oriented Formal Language and Method: 10th International Workshop, SOFL+MSVL 2020, Singapore, March 1, 2021, Revised Selected Papers (Theoretical Computer Science and General Issues)

✍ Scribed by Jinyun Xue (editor), Fumiko Nagoya (editor), Shaoying Liu (editor), Zhenhua Duan (editor)

• Publisher: Springer
• Year: 2021
• Tongue: English
• Leaves: 207
• Category: Library

✦ Synopsis

This book constitutes the refereed workshop proceedings of the 10th International Workshop on Structured Object-Oriented Formal Language and Method, SOFL+MSVL 2020, held in Singapore, in March 2021.
The 13 revised full papers included in the volume were carefully reviewed and selected from 24 submissions. They are organized in the following topical sections: modeling and specification; model checking; specification and verification; and testing and formal verification.Due to the Corona pandemic this event was held virtually.

✦ Table of Contents

Preface
Organization
Contents
Modeling and Specification
An MSVL-Based Modeling Framework for Back Propagation Neural Networks
1 Introduction
2 Background
2.1 The Language MSVL
2.2 Back Propagation Neural Network
3 Design of the Modeling Framework
3.1 Design Principles
3.2 Sketch of the Modeling Framework
3.3 Modeling of the Structure
3.4 Modeling of the Behavior
4 Implementation of the Modeling Framework
4.1 Implementation of the Data Structures
4.2 Implementation of Operations
4.3 Construction of a BP Neural Network
5 Experiment
6 Conclusions
References
A Case Study on Combining Agile Requirements Development and SOFL
1 Introduction
2 Background
3 Requirements Development Process
3.1 Informal Specification
3.2 Semi-formal Specification
3.3 A Combined Requirement Development Process
4 Case Study
4.1 Results
4.2 Findings
5 Related Work
6 Conclusions
References
Formal Modeling and Verification of Microservice-Based Cyber-Physical System
1 Introduction
2 Related Work
3 Microservice-Based CPS Framework
4 CSP
5 The Transformation Between MSBF and CSP
6 The Museum System Architecture
7 Museum System Modeling
8 The Verification of Museum System Model
9 Conclusion
References
Design and Implementation of Virtual Reality Geometric Modeling in Apla+VR
1 Introduction
2 Related Work
2.1 Virtual Reality Geometric Modeling
2.2 MAXScript Geometric Modeling Language and 3DSMax Framework
2.3 PAR Platform
3 Apla+VR Language Design and Code Generator Development
3.1 Apla+VR Syntax
3.2 Code Generator
3.3 Development Steps of Virtual Reality Models Based on PAR Method
4 A Case Study
4.1 Apla+VR Implementation of 3D Model
4.2 Generation
4.3 Formal Verification
5 Conclusions
References
Model Checking
An Unified Model Checking Approach of APTL
1 Introduction
2 Preliminaries
2.1 Alternating Projection Temporal Logic
2.2 From APTL Formulas to BCGs
3 Model Checking for APTL
3.1 Model Checking Algorithm for APTL
3.2 A Case Study
4 Conclusion
References
Model Checking Multi-interruption Concurrent Programs with TMSVL
1 Introduction
2 Model Checking Approach
3 Modeling Concurrent Programs with Interruption Using TMSVL
3.1 Modeling Single-Interruption Concurrent Programs
3.2 Modeling Multi-interruption Concurrent Programs
4 A Case Study
5 Conclusion
References
An MSVL Based Model Checking Method for Multi-threaded C Programs
1 Introduction
2 Preliminaries
2.1 Introduction of MSVL
2.2 Introduction of MSVL Semaphore
3 Model Checking Mutli-threaded C Program
3.1 Transforming C Program into MSVL Program
3.2 Validation Procedures
4 Case Study
4.1 Problem Description
5 Conclusion
References
Specification and Verification
A Formal Approach to Secure Design of RESTful Web APIs Using SOFL
1 Introduction
2 REST and SOFL
2.1 REST
2.2 SOFL
3 Our Proposed Approach
3.1 Step 1: Identification of Informal Functional and Security Requirements
3.2 Step 2: Transforming RAML Definitions to SOFL
3.3 Step 3: Formalization of API Specifications
4 Specification Based Conformance Testing
5 Case Study
6 Case Study Implementation Using Django REST Framework
7 Related Work
8 Conclusion and Future Works
References
Pointer Program Synthesis as Non-deterministic Planning
1 Introduction
2 FOND Planning
3 Symbolic Heaps
4 Symbolic Execution
5 Compiling Symbolic Execution into FOND Planning
6 Case Study and Experiment
7 Conclusion
References
Runtime Verification of Ethereum Smart Contracts Based on MSVL
1 Introduction
2 Preliminaries
2.1 MSVL
2.2 PPTL
3 Runtime Verification of Ethereum Smart Contracts
3.1 Framework
3.2 SOL2M Converter
3.3 Runtime Verification
4 Case Study: Runtime Verification for a Vote Smart Contract
5 Conclusion
References
Automatic Generation of Specification from Natural Language Based on Temporal Logic
1 Introduction
2 Background
2.1 PPTL
2.2 NLP Tools
3 Automatic Generation of Specification from Natural Language to Temporal Logic
3.1 Definition of Structured English Grammar
3.2 Formal Specification Generation
4 Case Study
4.1 Natural Language Tagging
4.2 Tag Recognition
4.3 Formula Generation
4.4 Decision of Formula Satisfiability
5 Related Work
6 Conclusions
References
Testing and Formal Verification
Software Testing with Statistical Partial Oracles
1 Introduction
2 Statistical Approach to Software Testing
2.1 Test Oracles
2.2 Statistical Test Oracles
3 Proposed Testing Framework
3.1 General Framework
3.2 Framework for Neural Networks Testing
3.3 Observers for Monitoring Neural Network States
4 A Case Study
4.1 MNIST Classification Problem
4.2 Overview of Testing Method
4.3 Semantic Noises
4.4 Solving Two Optimization Problems Interleaved
4.5 Controlled Experiment
4.6 Results and Discussions
5 Related Work
6 Concluding Remarks
References
Formalizing Spark Applications with MSVL
1 Introduction
2 Preliminaries
2.1 MSVL
3 Spark Framework
4 Principle for Formalizing Spark Applications
4.1 Data Storage System
4.2 Spark Operations
4.3 DAG-Based Formalization
4.4 Verifying Programs
5 Case Study: Word Count
5.1 Spark Application
5.2 Formalization
6 Conclusion
References
Author Index