Verifying of interface assertions for infinite state Mealy machines

作者：

Highlights：

• Interface assertions specifying the interface behavior of state machines.

• Verification of interface assertions for state machines by generalized invariants.

• Proof of liveness properties.

摘要

•Interface assertions specifying the interface behavior of state machines.•Verification of interface assertions for state machines by generalized invariants.•Proof of liveness properties.

论文关键词：Interactive Systems,I/O-machines,Specification,Verification,Invariants

论文评审过程：Received 18 August 2012, Revised 12 February 2014, Accepted 3 March 2014, Available online 17 March 2014.

论文官网地址：https://doi.org/10.1016/j.jcss.2014.03.002