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

BROOK

Model Checking Multi-interruption Concurrent Programs with TMSVLion concurrent programs, such as safety and liveness properties. The formal syntax and semantics of multi-interruption concurrent programs is established based on TMSVL, and the correctness and practicability of our approach is demonstrated with a case study.

落叶剂

Automatic Generation of Specification from Natural Language Based on Temporal Logicity of a PPTL formula generated by PPTLGenerator is checked by a tool PPTLSAT. Finally, to illustrate the principle and effectiveness of the framework, a case study of the safety property of Level 3 autonomous car is provided.

Complement

Insensate

hedonic

Foment

会议

GROUP

英寸

https://doi.org/10.1007/978-3-030-77474-5formal methods; modeling and specification; model checking; software verification; automatic transformat

和谐

978-3-030-77473-8Springer Nature Switzerland AG 2021