The formal design and development of multi-agent systems has attracted a considerable attention over the past decades because of their extensive use in safety-critical applications. This paper presents an efficient, hybrid and scalable formal development approach for safety-critical systems based on the multi-agent paradigm. In fact, we aim in this paper to benefit from the advantages of existing tools and techniques for each development stage and then integrate them in one unified approach. In particular approach, we advocate using Petri nets and rewriting logic to facilitate the formalization of multi-agent based systems, as well as we have integrated both the model checking and property-based testing techniques in the verification and testing stages. For illustrating the utilization and effectiveness of the proposed approach, we use it to analyze a simple automated distributing machine.
AguilarL.LalithM. and HoriM., Time critical mass evacuation simulation combining a multi-agent system and high-performance computing, Multi-agent Systems, 2017, p. 17.
2.
AkhtarN. and HussainS., Formal modeling of a mail transport system based on multi-agent system-of-systems, Journal of Information Communication Technologies and Robotic Applications, 2019, pp. 68–79.
3.
AkhtarN. and MissenM.M.S., Contribution to the formal specification and verification of a multi-agent robotic system, arXiv preprint arXiv:1604.05577, 2015.
4.
AlbertiM.DaolioD.TorroniP.GavanelliM.LammaE. and MelloP., Specification and verification of agent interaction protocols in a logic-based system, In Proceedings of the 2004 ACM symposium on Applied computing, ACM, 2004, pp. 72–78.
5.
AlexanderR. and KellyT., Supporting systems of systems hazard analysis using multi-agent simulation, Safety Science51(1) (2013), 302–318.
6.
AoumeurN. and SaakeG., Integrating and rapid-prototyping uml structural and behavioural diagrams using rewriting logic, In CAiSE, Springer, 2002, pp. 296–310.
7.
ArkiO.ZitouniA.DibE. and TakiA., A multi-agent security framework for cloud data storage, Multiagent and Grid Systems14(4) (2018), 357–382.
8.
AstefanoaeiL.DastaniM.MeyerJ.-J.C. and de BoerF.S., On the semantics and verification of normative multi-agent systems, J UCS15(13) (2009), 2629–2652.
9.
BarwellA.D.BrownC.HammondK.TurekW. and ByrskiA., Using program shaping and algorithmic skeletons to parallelise an evolutionary multi-agent system in erlang, Computing and Informatics35(4) (2017), 792–818.
10.
BauerB. and OdellJ., Uml 2.0 and agents: how to build agent-based systems with the new uml standard, Engineering Applications of Artificial Intelligence18(2) (2005), 141–157.
11.
BelalaF. and BoucheritA., A contribution to the formal checking of multi-agents systems, In IEEE International Conference on Computer Systems and Applications, 2006, IEEE, 2006, pp. 9–16.
12.
BenabdellahA.C.BouhaddouI. and BenghabritA., Supply chain challenges with complex adaptive system perspective, In World Conference on Information Systems and Technologies Springer, 2018, pp. 1081–1093.
13.
Benac EarleC. and FredlundL.-Å., A property-based testing framework for multi-agent systems, In Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, IFAAMAS, 2019, pp. 1823–1825.
14.
BenerecettiM. and CimattiA., Symbolic model checking for multi-agent systems, Proc. MoChart2 (2002), 1–8.
15.
BirdseyL.SzaboC. and FalknerK., Casl: a declarative domain specific language for modeling complex adaptive systems, In Proceedings of the 2016 Winter Simulation Conference, IEEE Press, 2016, pp. 1241–1252.
16.
BordiniR.H.FisherM.PardavilaC.VisserW. and WooldridgeM., Model checking multi-agent programs with casp, In International Conference on Computer Aided Verification, Springer, 2003, pp. 110–113.
17.
BordiniR.H.FisherM.PardavilaC. and WooldridgeM., Model checking agentspeak, In Proceedings of the second international joint conference on Autonomous agents and multiagent systems, ACM, 2003, pp. 409–416.
18.
BoucheritA.KhababaA. and CastroL.M., Automatic generating algorithm of rewriting logic specification for multi-agent system models based on petri nets, Multiagent and Grid Systems14(4) (2018), 403–418.
19.
BoudiafN.MokhatiF. and BadriM., Supporting formal verification of dima multi-agents models: towards a framework based on maude model checking, International Journal of Software Engineering and Knowledge Engineering18(7) (2008), 853–875.
20.
BrahimiS.MaamriR. and SahnounZ., Dynamic verification of hierarchical multi-agent plans, Multiagent and Grid Systems13(2) (2017), 113–142.
21.
BroyM. and CengarleM.V., Uml formal semantics: lessons learned, Software and Systems Modeling10(4) (2011), 441–446.
22.
BulutE.KhadraouiD. and MarquetB., Multi-agent based security assurance monitoring system for telecommunication infrastructures, In Proceedings of the Fourth IASTED International Conference on Communication, Network and Information Security, ACTA Press, 2007, pp. 90–95.
23.
CalvaresiD.AlbaneseG.MarinoniM.DubossonF.SernaniP.DragoniA.F. and SchumacherM., Timing reliability for local schedulers in multi-agent systems, In RTcMAS@ IJCAI, 2018, pp. 1–15.
24.
CalvaresiD.MarinoniM.SturmA.SchumacherM. and ButtazzoG., The challenge of real-time multi-agent systems for enabling iot and cps, In Proceedings of the international conference on web intelligence, ACM, 2017, pp. 356–364.
25.
CardelliniV.CasalicchioE. and GalliE., Agent-based modeling of interdependencies in critical infrastructures through uml, In Proceedings of the 2007 spring simulation multiconference-Volume 2, Society for Computer Simulation International, 2007, pp. 119–126.
26.
CarreraÁ.IglesiasC.A. and GarijoM., Beast methodology: An agile testing methodology for multi-agent systems based on behaviour driven development, Information Systems Frontiers16(2) (2014), 169–182.
27.
CastroL.M.LamelaP. and ThompsonS., Making property-based testing easier to read for humans, Computing and Informatics35(4) (2017), 890–913.
28.
CervenkaR. and TrencanskyI., The Agent Modeling Language-AML: A Comprehensive Approach to Modeling Multi-Agent Systems, Springer Science & Business Media, 2007.
29.
ChatterjeeR.K.NehaN. and SarkarA., Behavioral modeling of multi agent system: high level petri net based approach, International Journal of Agent Technologies and Systems (IJATS)7(1) (2015), 55–78.
30.
ChatterjeeR.K.SarkarA. and BhattacharyaS., Modeling and analysis of agent oriented system: Petri net based approach, In Proceedings of the International Conference on Software Engineering Research and Practice (SERP’11), 2011, pp. 17–23.
31.
ChennoufiM.BendellaF. and BouzidM., Multi-agent simulation collision avoidance of complex system: application to evacuation crowd behavior, International Journal of Ambient Computing and Intelligence (IJACI)9(1) (2018), 43–59.
32.
ClavelM.DuránF.EkerS.EscobarS.LincolnP.Martí-OlietN. and TalcottC., Two decades of maude, In Logic, Rewriting, and Concurrency, Springer, 2015, pp. 232–254.
33.
DarragiN.El-KoursiE. and Collart-DutilleulS., Architecture description language for cyber physical systems analysis: a railway control system case study, Computers in Railways XIV: Railway Engineering Design and Optimization135 (2014), 227–237.
34.
DerrickJ.WalkinshawN.ArtsT.Benac EarleC.CesariniF.FredlundL.-A.GuliasV.HughesJ. and ThompsonS., Property-based testing – the protest project, LNCS6286 LNCS: 250–271, 2010.
35.
DibA.T. and SahnounZ., Formal specification of multi-agent system architecture, In ICAASE, 2014, pp. 65–72.
36.
DillonD.S.DillonT.S. and ChangE., Using uml 2.1 to model multi-agent systems, In Software Technologies for Embedded and Ubiquitous Systems, Springer, 2008, pp. 1–8.
37.
D’SouzaS.RaoA.SharmaA. and SinghS., Modeling and verification of a multi-agent argumentation system using nusmv, arXiv preprint arXiv:1209.4330, 2012.
38.
EhikioyaS.A. and ZhangC., Real-time multi-agents architecture for e-commerce servers, International Journal of Networked and Distributed Computing6(2) (2018), 88–98.
39.
EkerS.MeseguerJ. and SridharanarayananA., The maude ltl model checker, Electronic Notes in Theoretical Computer Science71 (2004), 162–187.
40.
EmadiS. and ShamsF., Transformation of usecase and sequence diagrams to petri nets, In Computing, Communication, Control, and Management, 2009. CCCM 2009. ISECS International Colloquium on, volume 4, IEEE, 2009, pp. 399–403.
41.
FantechiA. and PepiS., Petri nets modeling for the schedulability analysis of industrial real time systems, In AMARETTO@ MODELSWARD, 2016, pp. 5–13.
42.
FernandesJ.M., Combining petri nets and uml for model-based software engineering, CEUR Workshop Proceedings, 2012.
43.
FigatM. and ZielińskiC., Methodology of designing multi-agent robot control systems utilising hierarchical petri nets, arXiv preprint arXiv:1906.11614, 2019.
44.
FrasheriM.TrinhL.A.CürüklüB. and EkströmM., Failure analysis for adaptive autonomous agents using petri nets, In 2017 Federated Conference on Computer Science and Information Systems (FedCSIS), IEEE, 2017, pp. 293–297.
45.
GammieP. and Van Der MeydenR., Mck: Model checking the logic of knowledge, In International Conference on Computer Aided Verification, Springer, 2004, pp. 479–483.
46.
GarlanD.SchmerlB.R. and ChengS.-W., Software architecture-based self-adaptation, Autonomic Computing and Networking1 (2009), 31–55.
47.
GlaschenkoA.IvaschenkoA.RzevskiG. and SkobelevP., Multi-agent real time scheduling system for taxi companies, In 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2009), Budapest, Hungary, 2009, pp. 29–36.
48.
GonçalvesE.J.T.CortesM.I.CamposG.A.L.LopesY.S.FreireE.S.da SilvaV.T.de OliveiraK.S.F. and de OliveiraM.A., Mas-ml 2.0: Supporting the modelling of multi-agent systems with different agent architectures, Journal of Systems and Software108 (2015), 77–109.
49.
GroceA.HolzmannG. and JoshiR., Randomized differential testing as a prelude to formal verification, In 29th International Conference on Software Engineering (ICSE’07), IEEE, 2007, pp. 621–631.
50.
GuanH., Prevention and control model of enterprise business risk based on multi-agent, Journal of Convergence Information Technology5(7) (2010), 148–154.
51.
HeinerM.SchwarickM. and WegenerJ.-T., Charlie–an extensible petri net analysis tool, In International Conference on Applications and Theory of Petri Nets and Concurrency, Springer, 2015, pp. 200–211.
52.
HendrixJ.MeseguerJ. and SasseR., Maude itp 2.0 tutorial, Technical report, Technical report, University of Illinois at Urbana-Champaign, 2008.
53.
HsiehF.-S., Developing cooperation mechanism for multi-agent systems with petri nets, Engineering Applications of Artificial Intelligence22(4–5) (2009), 616–627.
54.
HsiehF.-S., A hybrid and scalable multi-agent approach for patient scheduling based on petri net models, Applied Intelligence47(4) (2017), 1068–1086.
55.
HuangY.-S.ChungT.-H. and SuP.-J., Synthesis of deadlock prevention policy using petri nets reachability graph technique, Asian Journal of Control12(3) (2010), 336–346.
56.
HughesJ.NorellU.SmallboneN. and ArtsT., Find more bugs with quickcheck! In Proceedings of the 11th International Workshop on Automation of Software Test, ACM, 2016, pp. 71–77.
57.
JuniorM.N.MacielP.LimaR.RibeiroA.OliveiraC.ArcoverdeA.BarretoR.TavaresE. and AmorinL., A retargetable environment for power-aware code evaluation: An approach based on coloured petri net, LNCS37282005, 49.
58.
KacprzakM.NabiałekW.NiewiadomskiA.PenczekW.PółrolaA.SzreterM.WoźnaB. and ZbrzeznyA., Verics 2007-a model checker for knowledge and real-time, Fundamenta Informaticae85(1–4) (2008), 313–328.
59.
KongJ. and LomuscioA., Symbolic model checking multi-agent systems against ctl* k specifications, In Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, IFAAMAS, 2017, pp. 114–122.
60.
KouvarosP. and LomuscioA., Automatic verification of parameterised multi-agent systems, In Proceedings of the 2013 international conference on Autonomous agents and multi-agent systems, IFAAMAS, 2013, pp. 861–868.
61.
LaouadiM.A.MokhatiF. and Seridi-BouchelaghemH., A formal framework for organization-centered multi-agent system specification: A rewriting logic based approach, Multiagent and Grid Systems13(4) (2017), 395–419.
62.
LiuC.L.KazmierczakE. and MillerT., A safety analysis method for multi-agent systems, International Journal of Computer and Information Engineering9(10) (2017), 2310–2319.
63.
LiuZ.ChenZ.SunH. and HuY., Multi agent system based process control in wide area protection against cascading events, In 2013 IEEE Grenoble Conference, IEEE, 2013, pp. 1–6.
64.
LomuscioA.PecheurC. and RaimondiF., Automatic verification of knowledge and time with nusmv, In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, IJCAI/AAAI Press, 2007, pp. 1384–1389.
65.
LomuscioA. and RaimondiF., Mcmas: A model checker for multi-agent systems, In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2006, pp. 450–454.
66.
MarzouguiB. and BarkaouiK., Interaction protocols in multi-agent systems based on agent petri nets model, Int J Adv Comput Sci Appl4(7) (2013).
67.
MazouziH.SeghrouchniA.E.F. and HaddadS., Open protocol design for complex interactions in multi-agent systems, In Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, ACM, 2002, pp. 517–526.
68.
MeseguerJ., Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science96(1) (1992), 73–155.
69.
MokhatiF. and BadriM., Generating maude specifications from uml use case diagrams, Journal of Object Technology8(2) (2009), 319–136.
70.
MouratidisH.KolpM.GiorginiP. and FaulknerS., An architectural description language for secure multi-agent systems, Web Intelligence and Agent Systems: An International Journal8(1) (2010), 99–122.
71.
Nguyen-DucM.GuessoumZ.MarinO.PerrotJ.-F. and BriotJ.-P., A multi-agent approach to reliable air traffic control, na, 2008.
72.
NiaziM.A.HussainA. and KolbergM., Verification & validation of agent based simulations using the vomas (virtual overlay multi-agent system) approach, arXiv preprint arXiv:1708.02361, 2017.
73.
OclO., 2.0 specification, Final Adopted Specification ptc/03-10, 14, 2005.
74.
ÖlveczkyP.C.BoronatA. and MeseguerJ., Formal semantics and analysis of behavioral aadl models in real-time maude, In Formal Techniques for Distributed Systems, Springer, 2010, pp. 47–62.
75.
ParaskevopoulouZ.HriţcuC.DénèsM.LampropoulosL. and PierceB.C., Foundational property-based testing, In International Conference on Interactive Theorem Proving, Springer, 2015, pp. 325–343.
76.
PereverzevaI.TroubitsynaE. and LaibinisL., Formal development of critical multi-agent systems: A refinement approach, In 2012 Ninth European Dependable Computing Conference, IEEE, 2012, pp. 156–161.
77.
PipattanasompornM.FerozeH. and RahmanS., Securing critical loads in a pv-based microgrid with a multi-agent system, Renewable Energy39(1) (2012), 166–174.
78.
PodorozhnyR.KhurshidS.PerryD. and ZhangX., Verification of multi-agent negotiations using the alloy analyzer, In International Conference on Integrated Formal Methods, Springer, 2007, pp. 501–517.
79.
PrzigodaN.HilkenC.WilleR.PeleskaJ. and DrechslerR., Checking concurrent behavior in uml/ocl models, In 2015 ACM/IEEE 18th International Conference on Model Driven Engineering Languages and Systems (MODELS), IEEE, 2015, pp. 176–185.
80.
PujariS. and MukhopadhyayS., Petri net: A tool for modeling and analyze multi-agent oriented systems, International Journal of Intelligent Systems and Applications4(10) (2012), 103.
81.
RamatE., Introduction à la modélisation et à la simulation à événements discrets, Modélisation et simulation multi-agents: Applications pour les sciences de I’homme et de la société, 2006, pp. 50–73.
82.
RathS.K. et al., Analysis and modeling of a safety critical system using petri-net model, In 2016 1st India International Conference on Information Processing (IICIP), IEEE, 2016, pp. 1–6.
83.
ReisigW., A primer in Petri net design, Springer Science & Business Media, 2012.
84.
RenaultX.KordonF. and HuguesJ., Adapting models to model checkers, a case study: Analysing aadl using time or colored petri nets, In Rapid System Prototyping, 2009. RSP’09. IEEE/IFIP International Symposium on, IEEE, 2009, pp. 26–33.
85.
RenaultX.KordonF. and HuguesJ., From aadl architectural models to petri nets: Checking model viability, In Object/Component/Service-Oriented Real-Time Distributed Computing, 2009. ISORC’09. IEEE International Symposium on, IEEE, 2009, pp. 313–320.
86.
RislerM. and von StrykO., Formal behavior specification of multi-robot systems using hierarchical state machines in xabsl, In AAMAS08-workshop on formal models and methods for multi-robot systems, Estoril, Portugal. Citeseer, 2008.
87.
SatchidanandaD.SusmitaG. and Sung-baeC., Integration of swarm intelligence and artificial neural network, volume 78, World Scientific, 2011.
88.
SilvaC.GonçalvesE.DimuroG.DimuroG. and de Manuel JerezE., Modeling agent periodic routines in agent-based social simulation using colored petri nets, In 2013 BRICS Congress on Computational Intelligence and 11th Brazilian Congress on Computational Intelligence, IEEE, 2013, pp. 644–650.
89.
ŠimoňákS. and TomášekM., Acp semantics for petri nets, Computing and Informatics37(6) (2019), 1464–1484.
90.
SinghL.K. and RajputH., Dependability analysis of safety critical real-time systems by using petri nets, IEEE Transactions on Control Systems Technology26(2) (2017), 415–426.
91.
SkobelevP., Multi-agent systems for real-time adaptive resource management, In Industrial Agents, Elsevier, 2015, pp. 207–229.
92.
SmaaliS.ChoutriA. and BelalaF., K semantics for dynamic software architectures, In Proceedings of the International Arab Conference on Information Technology (ACIT ’2013), 2013.
93.
SouriA. and NavimipourN.J., Behavioral modeling and formal verification of a resource discovery approach in grid computing, Expert Systems with Applications41(8) (2014), 3831–3849.
94.
StehrM.-O.MeseguerJ. and ÖlveczkyP.C., Rewriting logic as a unifying framework for petri nets, In Unifying Petri Nets, Springer, 2001, pp. 250–303.
95.
SubburajV.H. and UrbanJ.E., Applying formal methods to specify security requirements in multi-agent systems, In 2018 Federated conference on computer science and information systems (FedCSIS), IEEE, 2018, pp. 707–714.
96.
SubburajV.H. and UrbanJ.E., Specifying security requirements in multi-agent systems using the descartes-agent specification language and auml, In Information technology for management: Emerging research and applications, Springer, 2018, pp. 93–111.
97.
van der AalstW. and BestE., Application and Theory of Petri Nets and Concurrency: 38th International Conference, PETRI NETS 2017, Zaragoza, Spain, June 25–30 2017, Proceedings, volume 10258. Springer, 2017.
98.
van RiemsdijkM.B.AştefănoaeiL. and de BoerF.S., Using the maude term rewriting language for agent development with formal foundations, In Specification and Verification of Multi-agent Systems, Springer, 2010, pp. 255–287.
99.
Van RiemsdijkM.B.De BoerF.S.DastaniM. and MeyerJ.-J.C., Prototyping 3apl in the maude term rewriting language, In International Workshop on Computational Logic in Multi-Agent Systems, Springer, 2006, pp. 95–114.
100.
WangJ.ShenR. and ZhuH., Agent oriented programming based on slabs, In Computer Software and Applications Conference, 2005. COMPSAC 2005. 29th Annual International, volume 1, IEEE, 2005, pp. 127–132.
101.
WendtA.WilkerS.MeiselM. and SauterT., A multi-agent-based middleware for the development of complex architectures, In 2018 IEEE 27th International Symposium on Industrial Electronics (ISIE), IEEE, 2018, pp. 723–728.
102.
WolfK., Petri net model checking with lola 2, In International Conference on Applications and Theory of Petri Nets and Concurrency, Springer, 2018, pp. 351–362.
103.
WooldridgeM.FisherM.HugetM.-P. and ParsonsS., Model checking multi-agent systems with mable, In Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, ACM, 2002, pp. 952–959.
104.
YangZ.HuK.MaD. and PiL., Towards a formal semantics for the aadl behavior annex, In Design, Automation & Test in Europe Conference & Exhibition, 2009. DATE’09, IEEE, 2009, pp. 1166–1171.
105.
YeungW.L., Behavioral modeling and verification of multi-agent systems for manufacturing control, Expert Systems with Applications38(11) (2011), 13555–13562.
106.
YuZ. and CaiY., Object-oriented petri nets based architecture description language for multi-agent systems, IJCSNS6(1) (2006), 123–131.
107.
ZhangY.-H.FanJ.-C. and LiaoX.-l., Simulation method of command and control process based on petri net [j], Journal of System Simulation7 (2012).
108.
ZhuH.HallP. and MayJ., Software unit test coverage and adequacy, ACM Computing Surveys29(4) (1997), 366–427.
109.
ZoumpoulakiA.AvradinisN. and VosinakisS., A multi-agent simulation framework for emergency evacuations incorporating personality and emotions, In Hellenic Conference on Artificial Intelligence, Springer, 2010, pp. 423–428.
110.
ZuritaN.F.S.ColbyM.K.TumerI.Y.HoyleC. and TumerK., Design of complex engineered systems using multi-agent coordination, Journal of Computing and Information Science in Engineering18(1) (2018), 011003.
