More Web Proxy on the site http://driver.im/

research-article

Verification of Distributed Systems via Sequential Emulation

Authors:

Luca Di Stefano,

Rocco De Nicola,

Omar InversoAuthors Info & Claims

ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 31, Issue 3

Article No.: 37, Pages 1 - 41

https://doi.org/10.1145/3490387

Published: 07 March 2022 Publication History

Abstract

Sequential emulation is a semantics-based technique to automatically reduce property checking of distributed systems to the analysis of sequential programs. An automated procedure takes as input a formal specification of a distributed system, a property of interest, and the structural operational semantics of the specification language and generates a sequential program whose execution traces emulate the possible evolutions of the considered system. The problem as to whether the property of interest holds for the system can then be expressed either as a reachability or as a termination query on the program. This allows to immediately adapt mature verification techniques developed for general-purpose languages to domain-specific languages, and to effortlessly integrate new techniques as soon as they become available. We test our approach on a selection of concurrent systems originated from different contexts from population protocols to models of flocking behaviour. By combining a comprehensive range of program verification techniques, from traditional symbolic execution to modern inductive-based methods such as property-directed reachability, we are able to draw consistent and correct verification verdicts for the considered systems.

References

[1]

Yehia Abd Alrahman, Rocco De Nicola, and Michele Loreti. 2020. Programming interactions in collective adaptive systems by relying on attribute-based communication. Science of Computer Programming 192 (2020), 102428. DOI:DOI:

Digital Library

[2]

Dana Angluin, James Aspnes, and David Eisenstat. 2008. A simple population protocol for fast robust approximate majority. Distributed Computing 21, 2 (2008), 87–102. DOI:DOI:

Digital Library

[3]

James Aspnes and Eric Ruppert. 2009. An introduction to population protocols. In Proceedings of the Middleware for Network Eccentric and Mobile Applications. Benoît Garbinato, Hugo Miranda, and Lúıs E. T. Rodrigues (Eds.). Springer, 97–120. DOI:DOI:

[4]

Alexander Bakst, Klaus von Gleissenthall, Rami Gökhan Kici, and Ranjit Jhala. 2017. Verifying distributed programs via canonical sequentialization. Proceedings of the ACM Programing Languages 1, OOPSLA (2017), 110:1–110:27. DOI:DOI:

Digital Library

[5]

M. Ballerini, N. Cabibbo, R. Candelier, A. Cavagna, E. Cisbani, I. Giardina, V. Lecomte, A. Orlandi, G. Parisi, A. Procaccini, M. Viale, and V. Zdravkovic. 2008. Interaction ruling animal collective behavior depends on topological rather than metric distance: Evidence from a field study. Proceedings of the National Academy of Sciences 105, 4 (2008), 1232–1237. DOI:DOI:

[6]

Dirk Beyer. 2016. Reliable and reproducible competition results with BenchExec and witnesses (report on SV-COMP 2016). In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Marsha Chechik and Jean-François Raskin (Eds.), Lecture Notes in Computer Science, Vol. 9636. Springer, 887–904. DOI:DOI:

Digital Library

[7]

Dirk Beyer. 2019. Automatic verification of C and Java programs: SV-COMP 2019. In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen (Eds.), Lecture Notes in Computer Science, Vol. 11429. Springer, 133–155. DOI:DOI:

[8]

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. 2007. The software model checker BLAST. Software Tools for Technology Transfer 9, 5–6 (2007), 505–525. DOI:DOI:

Digital Library

[9]

Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A tool for configurable software verification. In Proceedings of the 23rd International Conference on Computer Aided Verification. Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Lecture Notes in Computer Science, Vol. 6806. Springer, 184–190. DOI:DOI:

[10]

Dirk Beyer and Stefan Löwe. 2013. Explicit-state software model checking based on CEGAR and interpolation. In Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering. Vittorio Cortellessa and Dániel Varró (Eds.), Lecture Notes in Computer Science, Vol. 7793. Springer, 146–162. DOI:DOI:

Digital Library

[11]

Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems.Rance Cleaveland (Ed.), Lecture Notes in Computer Science, Vol. 1579. Springer, 193–207. DOI:DOI:

[12]

Michael Blondin, Javier Esparza, and Stefan Jaax. 2018. Peregrine: A tool for the analysis of population protocols. In Proceedings of the 30th International Conference on Computer Aided Verification. Hana Chockler and Georg Weissenbacher (Eds.), Lecture Notes in Computer Science, Vol. 10981. Springer, 604–611. DOI:DOI:

[13]

Eric Bonabeau, Marco Dorigo, and Guy Theraulaz. 1999. Swarm Intelligence: From Natural to Artificial Systems. Oxford University Press. Q335 .B59 1999

[14]

Rafael H. Bordini, Louise A. Dennis, Berndt Farwer, and Michael Fisher. 2008. Automated verification of multi-agent programs. In Proceedings of the 23rd International Conference on Automated Software Engineering. IEEE, 69–78. DOI:DOI:

Digital Library

[15]

Ahmed Bouajjani, Constantin Enea, Kailiang Ji, and Shaz Qadeer. 2018. On the completeness of verifying message passing programs under bounded asynchrony. In Proceedings of the 30th International Conference on Computer Aided Verification. Hana Chockler and Georg Weissenbacher (Eds.), Lecture Notes in Computer Science, Vol. 10982. Springer, 372–391. DOI:DOI:

[16]

Aaron R. Bradley. 2011. SAT-based model checking without unrolling. In Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation. Ranjit Jhala and David A. Schmidt (Eds.), Lecture Notes in Computer Science, Vol. 6538. Springer, 70–87. DOI:

[17]

Guillaume Brat, Jorge A. Navas, Nija Shi, and Arnaud Venet. 2014. IKOS: A framework for static analysis based on abstract interpretation. In Proceedings of the 12th International Conference on Software Engineering and Formal Methods. Lecture Notes in Computer Science, Vol. 8702. Springer, 271–277. DOI:DOI:

[18]

Marek Chalupa, Martina Vitovská, Martin Jonás, Jiri Slaby, and Jan Strejcek. 2017. Symbiotic 4: Beyond reachability - (competition contribution). In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Axel Legay and Tiziana Margaria (Eds.), Lecture Notes in Computer Science, Vol. 10206. Springer, 385–389. DOI:DOI:

Digital Library

[19]

Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, and Björn Wachter. 2015. Synthesising interprocedural bit-precise termination proofs. In Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering. IEEE, 53–64. DOI:DOI:

Digital Library

[20]

Alessandro Cimatti, Alberto Griggio, Andrea Micheli, Iman Narasamdya, and Marco Roveri. 2011. Kratos - a software model checker for SystemC. In Proceedings of the 23rd International Conference on Computer Aided Verification. Ganesh Gopalakrishnan and Shaz Qadeer (Eds.), Lecture Notes in Computer Science, Vol. 6806. Springer, 310–316. DOI:DOI:

[21]

Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A tool for checking ANSI-C programs. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Kurt Jensen and Andreas Podelski (Eds.). Lecture Notes in Computer Science, Springer, 168–176. DOI:DOI:

[22]

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2003. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM 50, 5 (2003), 752–794. DOI:DOI:

Digital Library

[23]

Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. 2012. TLA+ proofs. In Proceedings of the18th International Symposium on Formal Methods. Dimitra Giannakopoulou and Dominique Méry (Eds.), Lecture Notes in Computer Science, Vol. 7436. Springer, 147–154. DOI:DOI:

[24]

Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. 2015. Semantics-based generation of verification conditions by program specialization. In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming. Moreno Falaschi and Elvira Albert (Eds.). ACM, 91–102. DOI:DOI:

Digital Library

[25]

Rocco De Nicola. 2011. Process algebras. In Proceedings of the Encyclopedia of Parallel Computing. David A. Padua (Ed.). Springer, 1624–1636. DOI:DOI:

[26]

Rocco De Nicola, Luca Di Stefano, and Omar Inverso. 2020. Multi-agent systems with virtual stigmergy. Science of Computer Programming 187 (2020), 102345. DOI:DOI:

Digital Library

[27]

Rocco De Nicola, Tan Duong, and Omar Inverso. 2020. Verifying AbC specifications via emulation. In Proceedings of the 9th International Symposium on Leveraging Applications of Formal Methods. Tiziana Margaria and Bernhard Steffen (Eds.), Lecture Notes in Computer Science, Vol. 12477. Springer, 261–279. DOI:DOI:

Digital Library

[28]

Ankush Desai, Tommaso Dreossi, and Sanjit A. Seshia. 2017. Combining model checking and runtime verification for safe robotics. In Proceedings of the 17th International Conference on Runtime Verification. Shuvendu Lahiri and Giles Reger (Eds.), Lecture Notes in Computer Science, Vol. 10548. Springer, 172–189. DOI:DOI:

[29]

Luca Di Stefano, Rocco De Nicola, and Omar Inverso. 2021. Replication Package for the Paper: Verification of Distributed Systems via Sequential Emulation. (2021). DOI:DOI: accessed on January 6, 2022.

[30]

Luca Di Stefano, Frédéric Lang, and Wendelin Serwe. 2020. Combining SLiVER with CADP to analyze multi-agent systems. In Proceedings of the 22nd International Conference on Coordination Models and Languages. Simon Bliudze and Laura Bocchi (Eds.), Lecture Notes in Computer Science, Vol. 12134. Springer, 370–385. DOI:DOI:

Digital Library

[31]

Gilberto Echeverria, Séverin Lemaignan, Arnaud Degroote, Simon Lacroix, Michael Karg, Pierrick Koch, Charles Lesire, and Serge Stinckwich. 2012. Simulating complex robotic scenarios with MORSE. In Proceedings of the International Conference on Simulation, Modeling, and Programming for Autonomous Robots, Lecture Notes in Computer Science, Vol. 7628. Springer, 197–208. DOI:DOI:

Digital Library

[32]

Niklas Eén, Alan Mishchenko, and Robert K. Brayton. 2011. Efficient implementation of property directed reachability. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design. Per Bjesse and Anna Slobodová (Eds.). FMCAD Inc., 125–134.

Digital Library

[33]

Bernd Fischer, Omar Inverso, and Gennaro Parlato. 2013. CSeq: A concurrency pre-processor for sequential C verification tools. In Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering. Ewen Denney, Tevfik Bultan, and Andreas Zeller (Eds.). IEEE, 710–713. DOI:DOI:

Digital Library

[34]

Wan Fokkink. 2000. Introduction to Process Algebra. Springer.

[35]

Xiang Fu, Tevfik Bultan, and Jianwen Su. 2004. Conversation protocols: A formalism for specification and verification of reactive electronic services. Theoretical Computer Science 328, 1-2 (2004), 19–37. DOI:DOI:

Digital Library

[36]

Mikhail Y. R. Gadelha, Felipe R. Monteiro, Jeremy Morse, Lucas C. Cordeiro, Bernd Fischer, and Denis A. Nicole. 2018. ESBMC 5.0: An industrial-strength C model checker. In Proceedings of the ACM/IEEE International Conference on Automated Software Engineering. ACM, 888–891. DOI:DOI:

Digital Library

[37]

Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. 2011. CADP 2010: A toolbox for the construction and analysis of distributed processes. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 6605. Springer, 372–387. DOI:DOI:

[38]

Hubert Garavel, Frédéric Lang, and Wendelin Serwe. 2017. From LOTOS to LNT. In Proceedings of the ModelEd, TestEd, TrustEd - Essays Dedicated to Ed Brinksma on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, Vol. 10500. Springer, 3–26. DOI:DOI:

[39]

Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, and René Thiemann. 2017. Analyzing program termination and complexity automatically with AProVE. Journal of Automated Reasoning 58, 1 (2017), 3–31. DOI:DOI:

Digital Library

[40]

Susanne Graf and Hassen Saïdi. 1997. Construction of abstract state graphs with PVS. In Proceedings of the 9th International Conference on Computer Aided Verification. Orna Grumberg (Ed.), Lecture Notes in Computer Science, Vol. 1254. Springer, 72–83. DOI:DOI:

[41]

Jim Gray. 1978. Notes on data base operating systems. In Proceedings of the Operating Systems, An Advanced Course. Michael J. Flynn, Jim Gray, Anita K. Jones, Klaus Lagally, Holger Opderbeck, Gerald J. Popek, Brian Randell, Jerome H. Saltzer, and Hans-Rüdiger Wiehle (Eds.), Lecture Notes in Computer Science, Vol. 60. Springer, 393–481. DOI:DOI:

[42]

Volker Grimm, Eloy Revilla, Uta Berger, Florian Jeltsch, Wolf M. Mooij, Steven F. Railsback, Hans-Hermann Thulke, Jacob Weiner, Thorsten Wiegand, and Donald L. DeAngelis. 2005. Pattern-oriented modeling of agent-based complex systems: Lessons from ecology. Science 310, 5750 (2005), 987–991. DOI:DOI:

[43]

Matthias Güdemann, Pascal Poizat, Gwen Salaün, and Lina Ye. 2016. VerChor: A framework for the design and verification of choreographies. IEEE Transactions on Services Computing 9, 4 (2016), 647–660. DOI:DOI:

[44]

Henning Günther, Alfons Laarman, and Georg Weissenbacher. 2016. Vienna verification tool: IC3 for parallel software - (competition contribution). In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Marsha Chechik and Jean-François Raskin (Eds.), Lecture Notes in Computer Science, Vol. 9636. Springer, 954–957. DOI:DOI:

Digital Library

[45]

Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn verification framework. In Proceedings of the 27th International Conference on Computer Aided Verification. Daniel Kroening and Corina S. Pasareanu (Eds.), Lecture Notes in Computer Science, Vol. 9206. Springer, 343–361. DOI:DOI:

[46]

Peter Haglich, Christopher A. Rouff, and Laura Pullum. 2010. Detecting emergence in social networks. In Proceedings of the SocialCom/PASSAT. IEEE Computer Society, 693–696.

Digital Library

[47]

Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2013. Software model checking for people who love automata. In Proceedings of the 25th International Conference on Computer Aided Verification. Natasha Sharygina and Helmut Veith (Eds.), Lecture Notes in Computer Science, Vol. 8044. Springer, 36–52. DOI:DOI:

[48]

Carl Hewitt, Peter Boehler Bishop, and Richard Steiger. 1973. A universal modular ACTOR formalism for artificial intelligence. In Proceedings of the IJCAI. William Kaufmann, 235–245.

[49]

Francis Heylighen. 2016. Stigmergy as a universal coordination mechanism I: Definition and components. Cognitive Systems Research 38 (2016), 4–13. DOI:DOI:

Digital Library

[50]

C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall.

Digital Library

[51]

Christopher-Eyk Hrabia, Marco Lützenberger, and Sahin Albayrak. 2018. Towards adaptive multi-robot systems: Self-organization and self-adaptation. Knowledge Engineering Review 33 (2018), e16. DOI:DOI:

[52]

Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2014. Bounded model checking of multi-threaded C programs via lazy sequentialization. In Proceedings of the 26th International Conference on Computer Aided Verification. Armin Biere and Roderick Bloem (Eds.), Lecture Notes in Computer Science, Vol. 8559. Springer, 585–602. DOI:DOI:

Digital Library

[53]

Omar Inverso and Catia Trubiani. 2020. Parallel and distributed bounded model checking of multi-threaded programs. In Proceedings of the 25th Symposium on Principles and Practice of Parallel Programming. Rajiv Gupta and Xipeng Shen (Eds.). ACM, 202–216. DOI:DOI:

Digital Library

[54]

Adel Khaled and James Miller. 2017. Using \(\pi\)-calculus for formal modeling and verification of WS-CDL choreographies. IEEE Transactions on Services Computing 10, 2 (2017), 316–327. DOI:DOI:

[55]

James C. King. 1976. Symbolic execution and program testing. Communication of the ACM 19, 7 (1976), 385–394. DOI:DOI:

Digital Library

[56]

N. Koenig and A. Howard. 2004. Design and use paradigms for Gazebo, an open-source multi-robot simulator. In Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems, Vol. 3. IEEE, 2149–2154. DOI:DOI:

[57]

Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014. SMT-based model checking for recursive programs. In Proceedings of the 26th International Conference on Computer Aided Verification. Armin Biere and Roderick Bloem (Eds.), Lecture Notes in Computer Science, Vol. 8559. Springer, 17–34. DOI:DOI:

Digital Library

[58]

Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. 2019. TLA+ model checking made symbolic. PACMPL 3, OOPSLA (2019), 123:1–123:30. DOI:DOI:

Digital Library

[59]

Igor V. Konnov, Helmut Veith, and Josef Widder. 2017. On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability. Information and Computation 252 (2017), 95–109. DOI:DOI:

Digital Library

[60]

Savas Konur, Clare Dixon, and Michael Fisher. 2010. Formal verification of probabilistic swarm behaviours. In Proceedings of the 7th International Conference on Swarm Intelligence. Vol. 6234. Springer, 440–447. DOI:DOI:

[61]

Panagiotis Kouvaros and Alessio Lomuscio. 2015. A counter abstraction technique for the verification of robot swarms. In Proceedings of the 29th Conference on Artificial Intelligence. Blai Bonet and Sven Koenig (Eds.). AAAI, 2081–2088.

[62]

Johannes Lächele, Antonio Franchi, Heinrich H. Bülthoff, and Paolo Robuffo Giordano. 2012. SwarmSimX: Real-time simulation environment for multi-robot systems. In Proceedings of the International Conference on Simulation, Modeling, and Programming for Autonomous Robots. Itsuki Noda, Noriaki Ando, Davide Brugali, and James J. Kuffner (Eds.), Lecture Notes in Computer Science, Vol. 7628. Springer, 375–387. DOI:DOI:

Digital Library

[63]

Akash Lal and Thomas W. Reps. 2008. Reducing concurrent analysis under a context bound to sequential analysis. In Proceedings of the 20th International Conference on Computer Aided Verification. Aarti Gupta and Sharad Malik (Eds.), Lecture Notes in Computer Science, Vol. 5123. Springer, 37–51. DOI:DOI:

Digital Library

[64]

Leslie Lamport. 2002. Specifying Systems, the TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley.

[65]

Frédéric Lang, Radu Mateescu, and Franco Mazzanti. 2019. Compositional verification of concurrent systems by combining bisimulations. In Proceedings of the 3rd World Congress on Formal Methods. Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira (Eds.), Lecture Notes in Computer Science, Vol. 11800. Springer, 196–213. DOI:DOI:

Digital Library

[66]

Axel Legay, Benoît Delahaye, and Saddek Bensalem. 2010. Statistical model checking: An overview. In Proceedings of the International Conference on Runtime Verification. Howard Barringer, Yliès Falcone, Bernd Finkbeiner, Klaus Havelund, Insup Lee, Gordon J. Pace, Grigore Rosu, Oleg Sokolsky, and Nikolai Tillmann (Eds.), Lecture Notes in Computer Science, Vol. 6418. Springer, 122–135. DOI:DOI:

[67]

Alessio Lomuscio and Edoardo Pirovano. 2018. Verifying emergence of bounded time properties in probabilistic swarm systems. In Proceedings of the 27th International Joint Conference on Artificial Intelligence. ijcai.org, 403–409. DOI:DOI:

[68]

Alessio Lomuscio, Hongyang Qu, and Franco Raimondi. 2017. MCMAS: An open-source model checker for the verification of multi-agent systems. Software Tools for Technology Transfer 19, 1 (2017), 9–30. DOI:DOI:

Digital Library

[69]

Sean Luke, Claudio Cioffi-Revilla, Liviu Panait, Keith Sullivan, and Gabriel Catalin Balan. 2005. MASON: A multiagent simulation environment. Simulation 81, 7 (2005), 517–527. DOI:DOI:

Digital Library

[70]

Maja J. Matarić. 1993. Designing emergent behaviors: From local interactions to collective intelligence. In Proceedings of the 2nd International Conference on Adaptive Behavior from Animals to Animats 2. MIT Press, 432–441.

[71]

Robin Milner. 1975. Processes: A mathematical model of computing agents. In Proceedings of the Logic Colloquium’73. Studies in Logic and the Foundations of Mathematics, Vol. 80. Elsevier, 157–173. DOI:DOI:

[72]

Robin Milner. 1980. A Calculus of Communicating Systems. LNCS, Vol. 92. Springer. DOI:DOI:

[73]

Robin Milner. 1989. Communication and Concurrency. Prentice Hall.

Digital Library

[74]

Peter D. Mosses. 2004. Modular structural operational semantics. Journal of Logic and Algebraic Programming 60-61 (2004), 195–228. DOI:DOI:

[75]

D. E Nadales Agut. 2012. A Compositional Interchange Format for Hybrid Systems: Design and Implementation. PhD Thesis. Technische Universiteit Eindhoven.

[76]

Reza Olfati-Saber. 2006. Flocking for multi-agent dynamic systems: Algorithms and theory. IEEE Transactions on Automatic Control 51, 3 (2006), 401–420. DOI:DOI:

[77]

OMG. 2010. Business Process Model And Notation - Version 2.0. Technical Report dtc/2010-05-03.

[78]

Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. 2016. Ivy: Safety verification by interactive generalization. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. Chandra Krintz and Emery Berger (Eds.). ACM, 614–630. DOI:DOI:

Digital Library

[79]

H. Van Dyke Parunak. 1997. “Go to the Ant”: Engineering principles from natural multi-agent systems. Annals of Operations Research 75 (1997), 69–101. DOI:DOI:

[80]

Anna Philippou, Mauricio Toro, and Margarita Antonaki. 2013. Simulation and verification in a process calculus for spatially-explicit ecological models. Scientific Annals of Computer Science 23, 1 (2013), 119–167. DOI:DOI:

[81]

Carlo Pinciroli, Adam Lee-Brown, and Giovanni Beltrame. 2015. A tuple space for data sharing in robot swarms. In Proceedings of the 9th EAI International Conference on Bio-Inspired Information and Communications Technologies. ICST/ACM, 287–294.

[82]

Carlo Pinciroli, Vito Trianni, Rehan O’Grady, Giovanni Pini, Arne Brutschy, Manuele Brambilla, Nithin Mathews, Eliseo Ferrante, Gianni Di Caro, Frederick Ducatelle, Mauro Birattari, Luca Maria Gambardella, and Marco Dorigo. 2012. ARGoS: A modular, parallel, multi-engine simulator for multi-robot systems. Swarm Intelligence 6, 4 (2012), 271–295. DOI:DOI:

[83]

Gordon D. Plotkin. 1981. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19. Computer Science Department, Aarhus University. Reprinted in J. Log. Algebr. Program., 2004.

[84]

Amir Pnueli. 1977. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science. IEEE, 46–57. DOI:DOI:

Digital Library

[85]

Shaz Qadeer and Jakob Rehof. 2005. Context-bounded model checking of concurrent software. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Nicolas Halbwachs and Lenore D. Zuck (Eds.), Lecture Notes in Computer Science, Vol. 3440. Springer, 93–107. DOI:DOI:

Digital Library

[86]

Zongyan Qiu, Xiangpeng Zhao, Chao Cai, and Hongli Yang. 2007. Towards the theoretical foundation of choreography. In Proceedings of the 16th International Conference on World Wide Web. Carey L. Williamson, Mary Ellen Zurko, Peter F. Patel-Schneider, and Prashant J. Shenoy (Eds.). ACM, 973–982. DOI:DOI:

Digital Library

[87]

Zvonimir Rakamaric and Michael Emmi. 2014. SMACK: Decoupling source language details from verifier implementations. In Proceedings of the 26th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, Vol. 8559. Springer, 106–113. DOI:DOI:

Digital Library

[88]

Thomas W. Reps, Susan Horwitz, and Shmuel Sagiv. 1995. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Ron K. Cytron and Peter Lee (Eds.). ACM, 49–61. DOI:DOI:

Digital Library

[89]

Craig W. Reynolds. 1987. Flocks, herds and schools: A distributed behavioral model. In Proceedings of the 14th Annual Conference on Computer Graphics and Interactive Techniques. Maureen C. Stone (Ed.), Vol. 21. ACM, 25–34. DOI:DOI:

Digital Library

[90]

Adrián Riesco. 2018. Model checking parameterized by the semantics in maude. In Proceedings of the 14th International Symposium on Functional and Logic Programming. John P. Gallagher and Martin Sulzmann (Eds.), Lecture Notes in Computer Science, Vol. 10818. Springer, 198–213. DOI:DOI:

[91]

Eric Rohmer, Surya P. N. Singh, and Marc Freese. 2013. V-REP: A versatile and scalable robot simulation framework. In Proceedings of the IEEE/RSJ International Conference on Intelligent Robots and Systems. IEEE, 1321–1326. DOI:DOI:

[92]

Nima Roohi and Gwen Salaün. 2011. Realizability and dynamic reconfiguration of chor specifications. Informatica 35, 1 (2011), 39–49.

[93]

Peter Schrammel and Daniel Kroening. 2016. 2LS for program analysis - (competition contribution). In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Marsha Chechik and Jean-François Raskin (Eds.), Lecture Notes in Computer Science, Vol. 9636. Springer, 905–907. DOI:DOI:

Digital Library

[94]

Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. Programming and proving with distributed protocols. PACMPL 2, POPL (2018), 28:1–28:30. DOI:DOI:

Digital Library

[95]

Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. 2000. Checking safety properties using induction and a SAT-solver. In Proceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design. Warren A. Hunt Jr. and Steven D. Johnson (Eds.), Lecture Notes in Computer Science, Vol. 1954. Springer, 108–125. DOI:DOI:

[96]

Andrei Stefanescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Rosu. 2016. Semantics-based program verifiers for all languages. In Proceedings of the SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. ACM, 74–91. DOI:DOI:

Digital Library

[97]

D. J. Sumpter, G. B. Blanchard, and D. S. Broomhead. 2001. Ants and agents: A process algebra approach to modelling ant colony behaviour. Bulletin of Mathematical Biology 63, 5 (2001), 951–980. DOI:DOI:

[98]

Ichiro Suzuki and Masafumi Yamashita. 1999. Distributed anonymous mobile robots: Formation of geometric patterns. SIAM Journal of Computing 28, 4 (1999), 1347–1363. DOI:DOI:

Digital Library

[99]

Leigh Tesfatsion. 2002. Agent-based computational economics: Growing economies from the bottom up. Artificial Life 8, 1 (2002), 55–82. DOI:DOI:

Digital Library

[100]

Guy Theraulaz and Eric Bonabeau. 1999. A brief history of stigmergy. Artificial Life 5, 2 (1999), 97–116. DOI:DOI:

Digital Library

[101]

Emil Vassev, Roy Sterritt, Christopher A. Rouff, and Mike Hinchey. 2012. Swarm technology at NASA: Building resilient systems. IT Professional 14, 2 (2012), 36–42.

Digital Library

[102]

Germán Vidal. 2015. Symbolic execution as a basis for termination analysis. Science of Computer Programming 102 (2015), 142–157. DOI:DOI:

Digital Library

[103]

W3C. 2005. Web Services Choreography Description Language - Version 1.0. Technical Report.

[104]

M. Winikoff. 2010. Assurance of agent systems: What role should formal verification play? In Proceedings of the Specification and Verification of Multi-Agent Systems. Springer. DOI:DOI:

[105]

Glynn Winskel. 1984. Synchronization trees. Theoretical Computer Science 34, 1-2 (1984), 33–82. DOI:DOI:

[106]

Yuan Yu, Panagiotis Manolios, and Leslie Lamport. 1999. Model checking TLA+ specifications. In Proceedings of the 10th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Laurence Pierre and Thomas Kropf (Eds.), Lecture Notes in Computer Science, Vol. 1703. Springer, 54–66. DOI:DOI:

Cited By

Shin YLee SChoi Y(2024)Non-Functional Requirements Discovery and Quality Assurance Using Goal Model for Earthquake Warning System in Operation2024 IEEE 32nd International Requirements Engineering Conference (RE)10.1109/RE59067.2024.00034(275-286)Online publication date: 24-Jun-2024
https://doi.org/10.1109/RE59067.2024.00034
Incerto ETrubiani C(2024)Flocks of Birds: A Quantitative EvaluationLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_17(271-286)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_17
Di Stefano LInverso O(2024)Emerging Synchrony in Applauding Audiences: Formal Analysis and SpecificationLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_16(253-270)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_16
Show More Cited By

Index Terms

Verification of Distributed Systems via Sequential Emulation

Recommendations

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Verification of Boolean programs with unbounded thread creation

Most symbolic software model checkers use abstraction techniques to reduce the verification of infinite-state programs to that of decidable classes. Boolean programs [T. Ball, S.K. Rajamani, Bebop: A symbolic model checker for Boolean programs, in: SPIN ...
A formally verified sequentializer for lustre-like concurrent synchronous data-flow programs
ICSE-C '17: Proceedings of the 39th International Conference on Software Engineering Companion

Synchronous data-flow languages (SDFL), such as Lustre [1], is a concurrent language that has been widely used in safety-critical systems. Verified compilers for such languages are crucial in generating trustworthy object code. A good approach is to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology

ACM Transactions on Software Engineering and Methodology Volume 31, Issue 3

July 2022

912 pages

ISSN:1049-331X

EISSN:1557-7392

DOI:10.1145/3514181

Editor:
Mauro Pezzè
USI Università della Svizzera italiana and SIT Schaffhausen Institute of Technology, Switzerland

Issue’s Table of Contents

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 March 2022

Accepted: 01 October 2021

Revised: 01 September 2021

Received: 01 January 2021

Published in TOSEM Volume 31, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Refereed

Funding Sources

MIUR

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
347
Total Downloads

Downloads (Last 12 months)84
Downloads (Last 6 weeks)5

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shin YLee SChoi Y(2024)Non-Functional Requirements Discovery and Quality Assurance Using Goal Model for Earthquake Warning System in Operation2024 IEEE 32nd International Requirements Engineering Conference (RE)10.1109/RE59067.2024.00034(275-286)Online publication date: 24-Jun-2024
https://doi.org/10.1109/RE59067.2024.00034
Incerto ETrubiani C(2024)Flocks of Birds: A Quantitative EvaluationLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_17(271-286)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_17
Di Stefano LInverso O(2024)Emerging Synchrony in Applauding Audiences: Formal Analysis and SpecificationLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_16(253-270)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_16
Perini Brogi CMaggesi M(2024)Analysing Collective Adaptive Systems by Proving TheoremsLeveraging Applications of Formal Methods, Verification and Validation. REoCAS Colloquium in Honor of Rocco De Nicola10.1007/978-3-031-73709-1_14(223-237)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-73709-1_14
De Nicola RDi Stefano LInverso OValiani S(2023)Modelling flocks of birds and colonies of ants from the bottom upInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-023-00731-025:5-6(675-691)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1007/s10009-023-00731-0
De Nicola RDi Stefano LInverso OValiani S(2023)Intuitive Modelling and Formal Analysis of Collective Behaviour in Foraging AntsComputational Methods in Systems Biology10.1007/978-3-031-42697-1_4(44-61)Online publication date: 9-Sep-2023
https://doi.org/10.1007/978-3-031-42697-1_4
De Nicola RDi Stefano LInverso OValiani S(2022)Process Algebras and Flocks of BirdsA Journey from Process Algebra via Timed Automata to Model Learning10.1007/978-3-031-15629-8_27(512-523)Online publication date: 7-Sep-2022
https://doi.org/10.1007/978-3-031-15629-8_27

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Full Text

View this article in Full Text.

HTML Format

View this article in HTML Format.

Media

Figures

Other

Tables

View full text|Download PDF

View Issue’s Table of Contents