Titlebook: Structured Object-Oriented Formal Language and Method; 10th International W Jinyun Xue,Fumiko Nagoya,Zhenhua Duan Conference proceedings 20

chance

An MSVL Based Model Checking Method for Multi-threaded C Programsodeling, Simulation and Validation Language (MSVL) is proposed. To this end, the rules for describing the parallel execution semantics of multi-threaded C program with MSVL are defined, , and a specific tool is developed for automatically translating a multi-threaded C program into its equivalent MS

离开

A Formal Approach to Secure Design of RESTful Web APIs Using SOFLer the network using HTTP and must not violate any of its security properties. When APIs are designed, the functional and security properties are inextricably linked thus security requirements of an API cannot be treated as afterthoughts. We therefore propose an approach to specifying and verifying

INCUR

Camouflage

Runtime Verification of Ethereum Smart Contracts Based on MSVLity problem of Ethereum smart contracts is more prominent due to its characteristics. Being a lightweight formal verification technique, runtime verification is pursued to check whether one monitored program execution obeys a desired property. In this paper, we propose a runtime verification method

Exposure

Automatic Generation of Specification from Natural Language Based on Temporal Logicthe effectiveness of formal specification generation and formal verification, this paper proposes a framework for automatic conversion from natural language describing properties to temporal logic formulas, and implements a tool PPTLGenerator (Propositional Projection Temporal Logic formula Generato

Inveterate

增强

Formalizing Spark Applications with MSVLcoming up with sequential implementations. Thus, formal verification is needed to guarantee the correctness of Spark applications. In order to verify Spark applications using verification tool ., this paper presents an approach to formalizing Spark applications with Modeling Simulation and Verificat

Aids209

peak-flow

An MSVL-Based Modeling Framework for Back Propagation Neural Networksworks can be constructed and trained according to the requirements of users. Experimental results show that these models have good performance in terms of metrics concerning training and prediction such as loss and accuracy.

Antecedent

A Case Study on Combining Agile Requirements Development and SOFLe combined requirement development process and observe reworks caused by requirement changes. The result shows that our proposed process is effective to define the data and constraints, though changes in domains’ properties need continuous studies.