@misc(Abrial1991,
 author       = {JR Abrial},
 year         = {1991},
 title        = {B-Tool Reference Manual. B-Core (UK) Ltd},
)
@article(Arbab2004,
 author       = {Farhad Arbab},
 year         = {2004},
 title        = {Reo: a channel-based coordination model for component composition},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {14},
 number       = {3},
 pages        = {329\begingroup\let \relax\relax \endgroup[Pleaseinsert\PrerenderUnicode{–}intopreamble]366},
 doi          = {10.1017/S0960129504004153},
)
@article(Arbab2006,
 author       = {Farhad Arbab},
 year         = {2006},
 title        = {Coordination for Component Composition},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {160},
 pages        = {15 -- 40},
 doi          = {10.1016/j.entcs.2006.05.013},
 note         = {Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 2005)},
)
@inproceedings(Arbab2008A,
 author       = {Farhad Arbab and Natallia Kokash and Sun Meng},
 year         = {2008},
 title        = {Towards using reo for compliance-aware business process modeling},
 booktitle    = {International Symposium On Leveraging Applications of Formal Methods, Verification and Validation},
 organization = {Springer},
 pages        = {108--123},
 doi          = {10.1007/978-3-540-88479-8\@uscore .9},
)
@inproceedings(Arbab2002A,
 author       = {Farhad Arbab and Jan JMM Rutten},
 year         = {2002},
 title        = {A coinductive calculus of component connectors},
 booktitle    = {International Workshop on Algebraic Development Techniques},
 organization = {Springer},
 pages        = {34--55},
 doi          = {10.1007/978-3-540-40020-2\@uscore .2},
)
@article(Atkinson2003,
 author       = {Colin Atkinson and Thomas Kuhne},
 year         = {2003},
 title        = {Model-driven development: a metamodeling foundation},
 journal      = {IEEE software},
 volume       = {20},
 number       = {5},
 pages        = {36--41},
 doi          = {10.1109/MS.2003.1231149},
)
@article(Baier2005,
 author       = {Christel Baier},
 year         = {2005},
 title        = {Probabilistic Models for Reo Connector Circuits},
 journal      = {J. UCS},
 volume       = {11},
 number       = {10},
 pages        = {1718--1748},
)
@article(Baier2006,
 author       = {Christel Baier and Marjan Sirjani and Farhad Arbab and Jan Rutten},
 year         = {2006},
 title        = {Modeling component connectors in Reo by constraint automata},
 journal      = {Science of computer programming},
 volume       = {61},
 number       = {2},
 pages        = {75--113},
 doi          = {10.1016/j.scico.2005.10.008},
)
@article(Benevides2018,
 author       = {Mario Benevides and Bruno Lopes and Edward Hermann Haeusler},
 year         = {2018},
 title        = {Towards reasoning about Petri nets: A Propositional Dynamic Logic based approach},
 journal      = {Theoretical Computer Science},
 volume       = {744},
 pages        = {22--36},
 doi          = {10.1016/j.tcs.2018.01.007},
)
@misc(Blackburn2001,
 author       = {Patrick Blackburn and De Rijke, M and Y Venema},
 year         = {2001},
 title        = {Cambridge tracts in theoretical computer science},
)
@article(Bruni2000,
 author       = {Roberto Bruni and Ugo Montanari},
 year         = {2000},
 title        = {Zero-safe nets: Comparing the collective and individual token approaches},
 journal      = {Information and computation},
 volume       = {156},
 number       = {1-2},
 pages        = {46--89},
 doi          = {10.1006/inco.1999.2819},
)
@inproceedings(Clarke2007,
 author       = {Dave Clarke},
 year         = {2007},
 title        = {Coordination: Reo, nets, and logic},
 booktitle    = {International Symposium on Formal Methods for Components and Objects},
 organization = {Springer},
 pages        = {226--256},
 doi          = {10.1007/978-3-540-92188-2\@uscore .10},
)
@inproceedings(Grilo2020-2,
 author       = {Erick Grilo and Bruno Lopes},
 year         = {2020},
 title        = {ReLo: a dynamic logic to reason about Reo circuits1},
 booktitle    = {Pre-Proceedings of the 15th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA)},
 pages        = {32},
)
@article(REOJAL,
 author       = {Erick Grilo and Daniel Toledo and Bruno Lopes},
 year         = {2022},
 title        = {A logical framework to reason about Reo circuits},
 journal      = {Journal of Applied Logics},
 volume       = {9},
 pages        = {199--254},
)
@incollection(Harel2001,
 author       = {David Harel and Dexter Kozen and Jerzy Tiuryn},
 year         = {2001},
 title        = {Dynamic logic},
 booktitle    = {Handbook of philosophical logic},
 publisher    = {Springer},
 pages        = {99--217},
 doi          = {10.1007/978-94-017-0456-4\@uscore .2},
)
@article(Jackson2002,
 author       = {Daniel Jackson},
 year         = {2002},
 title        = {Alloy: a lightweight object modelling notation},
 journal      = {ACM Transactions on Software Engineering and Methodology (TOSEM)},
 volume       = {11},
 number       = {2},
 pages        = {256--290},
 doi          = {10.1145/505145.505149},
)
@article(Jongmans2012,
 author       = {Sung-Shik TQ Jongmans and Farhad Arbab},
 year         = {2012},
 title        = {Overview of Thirty Semantic Formalisms for Reo.},
 journal      = {Scientific Annals of Computer Science},
 volume       = {22},
 number       = {1},
 doi          = {10.7561/SACS.2012.1.201},
)
@inproceedings(Klein2011,
 author       = {Joachim Klein and Sascha Kl{\"u}ppelholz and Andries Stam and Christel Baier},
 year         = {2011},
 title        = {Hierarchical modeling and formal verification. An industrial case study using Reo and Vereofy},
 booktitle    = {International Workshop on Formal Methods for Industrial Critical Systems},
 organization = {Springer},
 pages        = {228--243},
 doi          = {10.1007/978-3-642-24431-5\@uscore .17},
)
@inproceedings(Knight2002,
 author       = {John C Knight},
 year         = {2002},
 title        = {Safety critical systems: challenges and directions},
 booktitle    = {Proceedings of the 24th International Conference on Software Engineering},
 organization = {ACM},
 pages        = {547--550},
)
@article(Kokash2011,
 author       = {Natallia Kokash and Farhad Arbab},
 year         = {2011},
 title        = {Formal design and verification of long-running transactions with extensible coordination tools},
 journal      = {IEEE Transactions on Services Computing},
 volume       = {6},
 number       = {2},
 pages        = {186--200},
 doi          = {10.1109/TSC.2011.46},
)
@inproceedings(Kokash2010-2,
 author       = {Natallia Kokash and Behnaz Changizi and Farhad Arbab},
 year         = {2010},
 title        = {A semantic model for service composition with coordination time delays},
 booktitle    = {International Conference on Formal Engineering Methods},
 organization = {Springer},
 pages        = {106--121},
 doi          = {10.1007/978-3-642-16901-4\@uscore .9},
)
@article(Kokash2012,
 author       = {Natallia Kokash and Christian Krause and De Vink, Erik},
 year         = {2012},
 title        = {Reo+ mCRL2: A framework for model-checking dataflow in service compositions},
 journal      = {Formal Aspects of Computing},
 volume       = {24},
 number       = {2},
 pages        = {187--216},
 doi          = {10.1007/s00165-011-0191-6},
)
@inproceedings(Kokash2010,
 author       = {Natallia Kokash and Christian Krause and Erik P de Vink},
 year         = {2010},
 title        = {Data-aware design and verification of service compositions with Reo and mCRL2},
 booktitle    = {Proceedings of the 2010 ACM Symposium on Applied Computing},
 pages        = {2406--2413},
 doi          = {10.1145/1774088.1774590},
)
@article(Kripke1959,
 author       = {Saul A Kripke},
 year         = {1959},
 title        = {A completeness theorem in modal logic},
 journal      = {The journal of symbolic logic},
 volume       = {24},
 number       = {1},
 pages        = {1--14},
 doi          = {10.2307/2964568},
)
@article(Li2015,
 author       = {Yi Li and Meng Sun},
 year         = {2015},
 title        = {Modeling and verification of component connectors in Coq},
 journal      = {Science of Computer Programming},
 volume       = {113},
 pages        = {285--301},
 doi          = {10.1016/j.scico.2015.10.016},
)
@inproceedings(Li2017,
 author       = {Yi Li and Xiyue Zhang and Yuanyi Ji and Meng Sun},
 year         = {2017},
 title        = {Capturing Stochastic and Real-Time Behavior in Reo Connectors},
 booktitle    = {Formal Methods: Foundations and Applications - 20th Brazilian Symposium, {SBMF} 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings},
 pages        = {287--304},
 doi          = {10.1007/978-3-319-70848-5\kern.08em\vbox{\hrule width.35em height.6pt}\kern.08em18},
)
@article(Li2019,
 author       = {Yi Li and Xiyue Zhang and Yuanyi Ji and Meng Sun},
 year         = {2019},
 title        = {A Formal Framework Capturing Real-Time and Stochastic Behavior in Connectors},
 journal      = {Science of Computer Programming},
 doi          = {10.1016/j.scico.2019.02.005},
)
@article(Mousavi2006,
 author       = {Mohammad Reza Mousavi and Marjan Sirjani and Farhad Arbab},
 year         = {2006},
 title        = {Formal semantics and analysis of component connectors in Reo},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {154},
 number       = {1},
 pages        = {83--99},
 doi          = {10.1016/j.entcs.2005.12.034},
)
@inproceedings(Li2018,
 author       = {M. Saqib Nawaz and Meng Sun},
 year         = {2018},
 title        = {Reo2PVS: Formal Specification and Verification of Component Connectors},
 booktitle    = {The 30th International Conference on Software Engineering and Knowledge Engineering, Hotel Pullman, Redwood City, California, USA, July 1-3, 2018.},
 pages        = {391--390},
 doi          = {10.18293/SEKE2018-024},
)
@article(Ostro1992,
 author       = {Jonathan S Ostro},
 year         = {1992},
 title        = {Formal methods for the specification and design of real-time safety critical systems},
 journal      = {Journal of Systems and Software},
 volume       = {18},
 number       = {1},
 pages        = {33--60},
 doi          = {10.1016/0164-1212(92)90045-L},
)
@inproceedings(Papazoglou2003,
 author       = {Mike P Papazoglou},
 year         = {2003},
 title        = {Service-oriented computing: Concepts, characteristics and directions},
 booktitle    = {Web Information Systems Engineering, 2003. WISE 2003. Proceedings of the Fourth International Conference on},
 organization = {IEEE},
 pages        = {3--12},
 doi          = {10.1109/WISE.2003.1254461},
)
@article(Pourvatan2009,
 author       = {Bahman Pourvatan and Marjan Sirjani and Hossein Hojjat and Farhad Arbab},
 year         = {2009},
 title        = {Automated analysis of Reo circuits using symbolic execution},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {255},
 pages        = {137--158},
 doi          = {10.1016/j.entcs.2009.10.029},
)
@inproceedings(Sun2014,
 author       = {Meng Sun and Yi Li},
 year         = {2014},
 title        = {Formal modeling and verification of complex interactions in e-government applications},
 booktitle    = {Proceedings of the 8th International Conference on Theory and Practice of Electronic Governance},
 organization = {ACM},
 pages        = {506--507},
 doi          = {10.1145/2691195.2691296},
)
@article(Tasharofi2009,
 author       = {Samira Tasharofi and Marjan Sirjani},
 year         = {2009},
 title        = {Formal modeling and conformance validation for WS-CDL using Reo and CASM},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {229},
 number       = {2},
 pages        = {155--174},
 doi          = {10.1016/j.entcs.2009.06.034},
)
@inproceedings(Li2016,
 author       = {Xiyue Zhang and Weijiang Hong and Yi Li and Meng Sun},
 year         = {2016},
 title        = {Reasoning about connectors in Coq},
 booktitle    = {International Workshop on Formal Aspects of Component Software},
 organization = {Springer},
 pages        = {172--190},
 doi          = {10.1007/978-3-319-57666-4\@uscore .11},
)
@article(Zhang2019,
 author       = {Xiyue Zhang and Weijiang Hong and Yi Li and Meng Sun},
 year         = {2019},
 title        = {Reasoning about connectors using Coq and Z3},
 journal      = {Science of Computer Programming},
 volume       = {170},
 pages        = {27--44},
 doi          = {10.1016/j.scico.2018.10.002},
)