The concept of must testing is naturally parametrised with a chosen completeness criterion, defining the complete runs of a system. Here I employ justness as this completeness criterion, instead of the traditional choice of progress. The resulting must-testing preorder is incomparable with the default one, and can be characterised as the fair failure preorder of Vogler. It also is the coarsest precongruence preserving linear time properties when assuming justness. As my system model I here employ Petri nets with read arcs. Through their Petri net semantics, this work applies equally well to process algebras. I provide a Petri net semantics for a standard process algebra extended with signals; the read arcs are necessary to capture those signals.
翻译:必须测试的概念自然地与选择的完整性标准相仿,它定义了系统的完整运行。在这里,我使用公正作为完整性标准,而不是传统的进步选择。因此,必须测试的预排序与默认的不相容,可以被定性为沃格勒的公平故障预排序。这也是假设公正时保存线性时间属性的最粗略的预兼容性。由于我的系统模型I在这里使用Petri 网,并使用读弧。通过它们的Petri 网语义学,这项工作同样适用于代数处理。我为带有信号的标准代数进程代数提供了一种Petri 网语义学;读弧法对于捕捉这些信号是必要的。