When is `partial' adequate? A logic-based proof technique using partial specifications

ISCAS OpenIR

	When is `partial' adequate? A logic-based proof technique using partial specifications
	Cleaveland R.; Steffen B.
	1990
会议名称	Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e
会议日期	1990-06-04~1990-06-07
会议地点	Philadelphia, PA
收录类别	其他
合作性质	其它
ISBN	0-8186-2073-0
摘要	A technique is presented for ascertaining when a (finite-state) partial process specification is adequate, in the sense of being specified enough, for contexts in which it is to be used. The method relies on the automatic generation of a modal formula from the partial specification; if the remainder of the network satisfies this formula, then any process that meets the specification is guaranteed to ensure correct behavior of the overall system. Using the results, the authors develop compositional proof rules for establishing the correctness of networks of parallel processes and illustrate their use with several examples
语种	中文
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/1339
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Cleaveland R.,Steffen B.. When is `partial' adequate? A logic-based proof technique using partial specifications[C],1990.