Structured object-oriented formal language and method : 9th International Workshop, SOFL+MSVL 2019, Shenzhen, China, November 5, 2019, Revised selected papers /: 9th International Workshop, SOFL+MSVL 2019, Shenzhen, China, November 5, 2019, Revised selected papers. (2020)

• Record Type: Book
• Other Titles: SOFL+MSVL 2019
• Further Information: Note: Huaikou Miao, Cong Tian, Shaoying Liu, Zhenhua Duan (eds.).
• Other Names: Miao, Huaikou, 1953-; Tian, Cong; Liu, Shaoying, 1960-; Duan, Zhenhua; SOFL+MSVL (Workshop), 9th
• Contents: Intro -- Preface -- Organization -- Contents -- Testing and Debugging -- Analysis and Remodeling of the DirtyCOW Vulnerability by Debugging and Abstraction -- 1 Introduction -- 2 The DirtyCOW Vulnerability -- 3 Our Analysis of DirtyCOW -- 3.1 The Attack Path -- 3.2 Concrete State Transformation -- 3.3 Rebuilding of Control Flow Diagram -- 4 Remodeling of Related System Calls -- 4.1 State Abstraction -- 4.2 The Model Rebuilt -- 5 Related Work -- 6 Conclusion -- References -- A Formal Technique for Concurrent Generation of Software's Functional and Security Requirements in SOFL Specifications Abstract -- 1 Introduction -- 2 Related Works -- 3 Our Proposed Methodology -- 3.1 The Proposed Technique in Details -- 3.2 Adopted Attack Tree Analysis Algorithm -- 4 Case Study -- 4.1 Converting the SignUp Process into Its Equivalent System Functional Scenario Form -- 4.2 Deriving Operational Scenarios -- 4.3 Eliciting Potential Vulnerabilities for Each of the Derived Operational Scenarios -- 5 Discussions and Conclusions -- References -- Distortion and Faults in Machine Learning Software -- 1 Introduction -- 2 Machine Learning Software -- 2.1 Learning Programs -- 2.2 Inference Programs 2.3 Quality Issues -- 3 Distortion Degrees -- 3.1 Observations and Hypotheses -- 3.2 Generating Distorted Dataset -- 3.3 Some Properties -- 4 A Case Study -- 4.1 MNIST Classification Problem -- 4.2 Experiments -- 5 Discussions -- 5.1 Neuron Coverage -- 5.2 Test Input Generation -- 6 Concluding Remarks -- References -- A Divide & Conquer Approach to Testing Concurrent Java Programs with JPF and Maude -- 1 Introduction -- 2 Preliminaries -- 3 Specification-Based Concurrent Program Testing with a Simulation Relation -- 4 State Sequence Generation from Concurrent Programs -- 4.1 Java Pathfinder (JPF) 4.2 Generating State Sequences by JPF -- 5 A Divide & Conquer Approach to Generating State Sequences -- 6 A Divide & Conquer Approach to Testing Concurrent Programs -- 7 A Case Study: Alternating Bit Protocol (ABP) -- 8 Related Work -- 9 Conclusion -- References -- Formal Verification -- An Approach to Modeling and Verifying Multi-level Interrupt Systems with TMSVL -- 1 Introduction -- 2 Preliminaries -- 2.1 TPTL -- 2.2 TMSVL -- 3 Modeling of Multi-level Interrupt Systems -- 4 A Case Study -- 5 Conclusion -- References Towards Formal Verification of Neural Networks: A Temporal Logic Based Framework -- 1 Introduction -- 2 Background -- 2.1 MSVL -- 2.2 PPTL -- 2.3 MC -- 3 A Practical Verification Method for Neural Networks Based on MSVL -- 4 Case Study -- 5 Related Work -- 6 Conclusions -- References -- UMC4M: A Verification Tool via Program Execution -- 1 Introduction -- 2 Preliminaries -- 2.1 MSVL -- 2.2 PPTL -- 3 Design and Implementation of UMC4M -- 3.1 LNFG2MSVL -- 3.2 Multi-thread and Execute -- 3.3 PathCheck -- 4 Case Study -- 4.1 Description of the Dining Cryptographers Protocol
• Publisher Details: Cham : Springer
• Publication Date: 2020
• Extent: 1 online resource (366 pages)
• Subjects: 005.1; Formal methods (Computer science) -- Congresses; Object-oriented methods (Computer science) -- Congresses; Formal methods (Computer science); Object-oriented methods (Computer science); Electronic books; Electronic books; Conference papers and proceedings
• Languages: English
• ISBNs: 9783030414184; 3030414183
• Related ISBNs: 9783030414177
• Notes: Note: Print version record.
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.