位置：成果数据库 > 会议 > 会议详情页
Specifying and Verifying PLC systems with TLA+
  • 所属机构名称：清华大学
  • 成果类型：会议
  • 相关项目：基于定理证明的可信嵌入式软件建模与验证平台研究
同会议论文项目
基于定理证明的可信嵌入式软件建模与验证平台研究
期刊论文 16 会议论文 24 著作 1
同项目会议论文
Effective Predicate Abstraction for Program Verification
Modeling and Analysis of Real-life Job Shop Scheduling Problems by Petri nets
Modeling and Analysis of Stage Machinery Control Systems by Timed Colored Petri Nets
Formal specification and Code Generation of Programmable Logic Controllers
SimSoC: A full system simulation software for embedded systems
Translation-based model checking for PLC programs
Coq Modulo Theory - Short Paper
Formal Modeling and Verification of Services Managements for Pervasive Computing Environment
A Refinement-Based Validation Method for Programmable Logic Controllers
Parameterized Specification and Verification of PLC Systems in Coq
On Array Theory of Bounded Elements
Verifying Programmable Logic Controllers with Abstraction
A Maximum Weight Heuristic Method for Abstract State Computation
Formalization and Verfication of PLC Timers in Coq
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning
Compositional Abstraction Refinement for Timed Systems
A Computability Path Ordering for Polymorphic Terms
Specifying time-sensitive systems with TLA+
Data Mining Based Decomposition for Assume-Guarantee Reasoning
Certification of SAT of Solvers in Coq
The Testing Approach of Embedded Real-Time Automatic Control Software Based on Control Objects
On the relation between sized-types based termination and semantic labelling
A Computability Path Ordering for Polymorphic Terms - Short Paper