Published in Volume XXVIII, Issue 2, 2018, pages 289–337, doi: 10.7561/SACS.2018.2.289

Authors: A. Schinko, W. Vogler

Abstract

A refinement preorder for a model of concurrent systems should be compositional (i.e. a precongruence for parallel composition) and should not introduce faults into a fault-free specification. Arguably, the coarsest such precongruence is the optimal refinement preorder. For the model of interface automata, faults are communication errors in the form of unexpected inputs. The respective optimal preorder has been characterized as the inclusion of two trace sets. Here, we extend this result by regarding also quiescence (quiescence and divergence resp.) as faults. The latter preorder is coarser, i.e. better, than an earlier preorder regarding errors, quiescence and divergence. We also present conjunction operators for our settings, avoiding flaws that can be found in the literature, and a quotient operator.

Full Text (PDF)

References

[1] F. Aarts and F. W. Vaandrager. Learning I/O Automata. In CONCUR 2010, volume 6269 of LNCS, pages 71–85. Springer, 2010. doi:10.1007/978-3-642-15375-4_6.

[2] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A Theory of Communicating Sequential Processes. J. ACM, 31(3):560–599, 1984. doi:10.1145/828.833.

[3] F. Bujtor, S. Fendrich, G. Lüttgen, and W. Vogler. Nondeterministic Modal Interfaces. Theor. Comput. Sci., 642:24–53, 2016. doi:10.1016/ j.tcs.2016.06.011.

[4] F. Bujtor and W. Vogler. Error-Pruning in Interface Automata. Theor. Comput. Sci., 597:18–39, 2015. doi:10.1016/j.tcs.2015.06.047.

[5] C. Chilton, B. Jonsson, and M. Z. Kwiatkowska. An Algebraic Theory of Interface Automata. Theor. Comput. Sci., 549:146–174, 2014. doi:10.1016/j.tcs.2014.07.018.

[6] L. de Alfaro and T. A. Henzinger. Interface Automata. In ESEC/FSE 2001, pages 109–120. ACM, 2001. doi:10.1145/503209.503226.

[7] L. de Alfaro and T. A. Henzinger. Interface-Based Design. In Engineering Theories of Software Intensive Systems, pages 83–104. Springer, 2005. doi:10.1007/1-4020-3532-2_3.

[8] R. De Nicola and M. Hennessy. Testing Equivalences for Processes. Theor. Comput. Sci. 34, pages 83–133, 1984. doi:10.1016/0304-975(84)90113-0.

[9] D. L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, Cambridge, 1989.

[10] G. Lüttgen and W. Vogler. Conjunction on Processes: Full Abstraction Via Ready-Tree Semantics. Theor. Comput. Sci., 373(1-2):19–40, 2007. doi:10.1016/j.tcs.2006.10.022.

[11] B. Randell and M. Koutny. Failures: Their Definition, Modelling and Analysis. In ICTAC 2007, volume 4711 of LNCS, pages 260–274. Springer, 2007. doi:10.1007/978-3-540-75292-9_18.

[12] A. Schinko. Kommunikationsfehler, Verklemmung und Divergenz bei Interface-Automaten. B.Sc. Thesis, Universität Augsburg [obtainable from the author], 2016.

[13] R. Segala. Quiescence, Fairness, Testing, and the Notion of Implementation (Extended Abstract). In CONCUR ’93, volume 715 of LNCS, pages 324–338. Springer, 1993. doi:10.1007/3-540-57208-2_23.

[14] J. Tretmans. Test Generation With Inputs, Outputs, and Quiescence. In Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS ’96, volume 1055 of LNCS, pages 127–146. Springer, 1996. doi:10.1007/3-540-61042-1_42.

Bibtex

@article{sacscuza:schinko2018frfia,
  title={Fault-Free Refinements for Interface Automata},
  author={A. Schinko, W. Vogler},
  journal={Scientific Annals of Computer Science},
  volume={28},
  number={2},
  organization={``A.I. Cuza'' University, Ia\c si, Rom\^ania},
  year={2018},
  pages={289–337},
  publisher={``A.I. Cuza'' University Press, Ia\c si}
}