{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T15:00:31Z","timestamp":1773932431248,"version":"3.50.1"},"reference-count":62,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2022,9,3]],"date-time":"2022-09-03T00:00:00Z","timestamp":1662163200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,9,3]],"date-time":"2022-09-03T00:00:00Z","timestamp":1662163200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1007\/s10009-022-00665-z","type":"journal-article","created":{"date-parts":[[2022,9,3]],"date-time":"2022-09-03T18:04:47Z","timestamp":1662228287000},"page":"911-948","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Modeling and formal analysis of virtually synchronous cyber-physical systems in AADL"],"prefix":"10.1007","volume":"24","author":[{"given":"Jaehun","family":"Lee","sequence":"first","affiliation":[]},{"given":"Kyungmin","family":"Bae","sequence":"additional","affiliation":[]},{"given":"Peter Csaba","family":"\u00d6lveczky","sequence":"additional","affiliation":[]},{"given":"Sharon","family":"Kim","sequence":"additional","affiliation":[]},{"given":"Minseok","family":"Kang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,9,3]]},"reference":[{"key":"665_CR1","doi-asserted-by":"crossref","unstructured":"Steiner, W., Bauer, G., Hall, B., Paulitsch, M., Varadarajan, S.: TTEthernet dataflow concept. In: IEEE International Symposium on Network Computing and Applications, pp. 319\u2013322 (2009). IEEE","DOI":"10.1109\/NCA.2009.28"},{"issue":"6","key":"665_CR2","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1049\/cce:19990604","volume":"10","author":"G Leen","year":"1999","unstructured":"Leen, G., Heffernan, D., Dunne, A.: Digital networks in the automotive vehicle. Comput. Control Eng. J. 10(6), 257\u2013266 (1999)","journal-title":"Comput. Control Eng. J."},{"key":"665_CR3","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/j.scico.2014.09.011","volume":"103","author":"K Bae","year":"2015","unstructured":"Bae, K., Krisiloff, J., Meseguer, J., \u00d6lveczky, P.C.: Designing and verifying distributed cyber-physical systems using Multirate PALS: an airplane turning control system case study. Sci. Comput. Program. 103, 13\u201350 (2015)","journal-title":"Sci. Comput. Program."},{"key":"665_CR4","doi-asserted-by":"crossref","unstructured":"Arney, D., Jetley, R., Jones, P., Lee, I., Sokolsky, O.: Formal methods based development of a PCA infusion pump reference model: generic infusion pump (GIP) project. In: HCMDSS-MDPnP, pp. 23\u201333 (2007). IEEE","DOI":"10.1109\/HCMDSS-MDPnP.2007.36"},{"key":"665_CR5","doi-asserted-by":"crossref","unstructured":"Kim, C., Sun, M., Mohan, S., Yun, H., Sha, L., Abdelzaher, T.F.: A framework for the safe interoperability of medical devices in the presence of network failures. In: Proceedings of ICCPS, pp. 149\u2013158 (2010)","DOI":"10.1145\/1795194.1795215"},{"key":"665_CR6","volume-title":"Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control","year":"1996","unstructured":"Abrial, J., B\u00f6rger, E., Langmaack, H. (eds.): Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, vol. 1165. LNCS, Springer, Berlin (1996)"},{"key":"665_CR7","doi-asserted-by":"crossref","unstructured":"Al-Nayeem, A., Sun, M., Qiu, X., Sha, L., Miller, S.P., Cofer, D.D.: A formal architecture pattern for real-time distributed systems. In: Proceedings of RTSS, pp. 161\u2013170. IEEE, USA (2009)","DOI":"10.1109\/RTSS.2009.50"},{"key":"665_CR8","doi-asserted-by":"crossref","unstructured":"Miller, S., Cofer, D., Sha, L., Meseguer, J., Al-Nayeem, A.: Implementing logical synchrony in integrated modular avionics. In: Proceedings of IEEE\/AIAA 28th Digital Avionics Systems Conference. IEEE, USA (2009)","DOI":"10.1109\/DASC.2009.5347579"},{"key":"665_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2012.05.040","volume":"451","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J., \u00d6lveczky, P.C.: Formalization and correctness of the PALS architectural pattern for distributed real-time systems. Theor. Comput. Sci. 451, 1\u201337 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"665_CR10","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Kong, S., Gao, S., Clarke, E.M.: SMT-based analysis of virtually synchronous distributed hybrid systems. In: Proceedings of HSCC, pp. 145\u2013154. ACM, New York, NY, USA (2016)","DOI":"10.1145\/2883817.2883849"},{"key":"665_CR11","unstructured":"Feiler, P.H., Gluch, D.P.: Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis and Design Language. Addison-Wesley (2012)"},{"key":"665_CR12","doi-asserted-by":"crossref","unstructured":"Fran\u00e7a, R.B., Bodeveix, J.-P., Filali, M., Rolland, J.-F., Chemouil, D., Thomas, D.: The AADL Behaviour Annex\u2014experiments and roadmap. In: Proceedings of ICECCS. IEEE (2007)","DOI":"10.1109\/ICECCS.2007.41"},{"key":"665_CR13","volume-title":"All About Maude\u2014A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Lincoln, P., Mart\u00ed-Oliet, N., Talcott, C.: All About Maude\u2014A High-Performance Logical Framework, vol. 4350. LNCS, Springer, Berlin (2007)"},{"issue":"1","key":"665_CR14","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. J. Log. Algebraic Methods Program. 86(1), 269\u2013297 (2017)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"665_CR15","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1016\/j.scico.2019.03.006","volume":"178","author":"K Bae","year":"2019","unstructured":"Bae, K., Rocha, C.: Symbolic state space reduction with guarded terms for rewriting modulo SMT. Sci. Comput. Program. 178, 20\u201342 (2019)","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"665_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3182657","volume":"51","author":"R Baldoni","year":"2018","unstructured":"Baldoni, R., Coppa, E., D\u2019Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. (CSUR) 51(3), 1\u201339 (2018)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"665_CR17","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Proceedings of CAV. LNCS, vol. 8559, pp. 737\u2013744. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"665_CR18","doi-asserted-by":"crossref","unstructured":"Lee, J., Kim, S., Bae, K., \u00d6lveczky, P.C.: HybridSynchAADL: modeling and formal analysis of virtually synchronous CPSs in AADL. In: Proceedings of CAV\u201921. LNCS, vol. 12759, pp. 491\u2013504. Springer, Berlin (2021)","DOI":"10.1007\/978-3-030-81685-8_23"},{"issue":"5","key":"665_CR19","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1109\/32.815324","volume":"25","author":"J Rushby","year":"1999","unstructured":"Rushby, J.: Systematic formal verification for fault-tolerant time-triggered algorithms. IEEE Trans. Softw. Eng. 25(5), 651\u2013660 (1999)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"665_CR20","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C.: MSYNC: a generalized formal design pattern for virtually synchronous multirate cyber-physical systems. In: ACM Transactions on Embedded Computing Systems (Proceedings of EMSOFT\u201921), vol. 20, no. 5s, Article 105 (2021)","DOI":"10.1145\/3477036"},{"key":"665_CR21","doi-asserted-by":"crossref","unstructured":"Caspi, P., Mazuet, C., Paligot, N.R.: About the design of distributed control systems: the quasi-synchronous approach. In: International Conference on Computer Safety, Reliability, and Security (2001). Springer","DOI":"10.1007\/3-540-45416-0_21"},{"issue":"10","key":"665_CR22","doi-asserted-by":"publisher","first-page":"1300","DOI":"10.1109\/TC.2008.81","volume":"57","author":"S Tripakis","year":"2008","unstructured":"Tripakis, S., Pinello, C., Benveniste, A., Sangiovanni-Vincent, A., Caspi, P., Di Natale, M.: Implementing synchronous models on loosely time triggered architectures. IEEE Trans. Comput. 57(10), 1300\u20131314 (2008)","journal-title":"IEEE Trans. Comput."},{"key":"665_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2013.09.010","volume":"91","author":"K Bae","year":"2014","unstructured":"Bae, K., Meseguer, J., \u00d6lveczky, P.C.: Formal patterns for multirate distributed real-time systems. Sci. Comput. Program. 91, 3\u201344 (2014)","journal-title":"Sci. Comput. Program."},{"key":"665_CR24","doi-asserted-by":"crossref","unstructured":"Steiner, W., Rushby, J.: TTA and PALS: formally verified design patterns for distributed cyber-physical systems. In: 2011 IEEE\/AIAA 30th Digital Avionics Systems Conference, pp. 7\u201351 (2011). IEEE","DOI":"10.1109\/DASC.2011.6096120"},{"issue":"4","key":"665_CR25","first-page":"315","volume":"173","author":"S Skeirik","year":"2020","unstructured":"Skeirik, S., Stefanescu, A., Meseguer, J.: A constructor-based reachability logic for rewrite theories. Fund. Inform. 173(4), 315\u2013382 (2020)","journal-title":"Fund. Inform."},{"key":"665_CR26","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Escobar, S., Lincoln, P., Mart\u0131-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.: Maude manual (version 3.1). Technical report, SRI International, Menlo Park (2020). http:\/\/maude.cs.illinois.edu\/w\/index.php\/Maude_Manual_and_Examples"},{"issue":"1","key":"665_CR27","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"665_CR28","doi-asserted-by":"crossref","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV, pp. 171\u2013177 (2011). Springer","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"665_CR29","unstructured":"Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: version 2.0. In: SMT, vol. 13, p. 14 (2010)"},{"key":"665_CR30","doi-asserted-by":"crossref","unstructured":"Ahmad, E., Larson, B.R., Barrett, S.C., Zhan, N., Dong, Y.: Hybrid Annex: an AADL extension for continuous behavior and cyber-physical interaction modeling. In: Proceedings of ACM SIGAda Annual Conference on High Integrity Language Technology (HILT\u201914). ACM, New York (2014)","DOI":"10.1145\/2663171.2663178"},{"key":"665_CR31","doi-asserted-by":"crossref","unstructured":"Qian, Y., Liu, J., Chen, X.: Hybrid AADL: a sublanguage extension to AADL. In: Proceedings of Internetware\u201913. ACM, New York (2013)","DOI":"10.1145\/2532443.2532473"},{"key":"665_CR32","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J.: Definition, semantics, and analysis of multirate synchronous AADL. In: Proceedings of FM\u201914. LNCS, vol. 8442. Springer, Berlin (2014)","DOI":"10.1007\/978-3-319-06410-9_7"},{"key":"665_CR33","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Al-Nayeem, A., Meseguer, J.: Synchronous AADL and its formal analysis in Real-Time Maude. In: Proceedings of ICFEM\u201911, vol. 6991. LNCS, Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24559-6_43"},{"key":"665_CR34","doi-asserted-by":"crossref","unstructured":"\u00d6lveczky, P.C., Boronat, A., Meseguer, J.: Formal semantics and analysis of behavioral AADL models in Real-Time Maude. In: Formal Techniques for Distributed Systems, pp. 47\u201362. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-13464-7_5"},{"key":"665_CR35","doi-asserted-by":"crossref","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Proceedings of CADE, vol. 7898, pp. 208\u2013214. LNCS, Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-38574-2_14"},{"key":"665_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84800-015-5","volume-title":"Distributed Consensus in Multi-vehicle Cooperative Control","author":"W Ren","year":"2008","unstructured":"Ren, W., Beard, R.W.: Distributed Consensus in Multi-vehicle Cooperative Control. Springer, Berlin (2008)"},{"key":"665_CR37","doi-asserted-by":"crossref","unstructured":"Henzinger, T.: The theory of hybrid automata. In: Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265\u2013292. Springer, Berlin, Heidelberg (2000)","DOI":"10.1007\/978-3-642-59615-5_13"},{"key":"665_CR38","doi-asserted-by":"crossref","unstructured":"Bae, K., Gao, S.: Modular SMT-based analysis of nonlinear hybrid systems. In: Proceedings of FMCAD, pp. 180\u2013187. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102258"},{"key":"665_CR39","doi-asserted-by":"crossref","unstructured":"Raisch, J., Klein, E., Meder, C., Itigin, A., O\u2019Young, S.: Approximating automata and discrete control for continuous systems\u2014two examples from process control. In: Hybrid Systems V, pp. 279\u2013303. Springer, Berlin (1999)","DOI":"10.1007\/3-540-49163-5_16"},{"key":"665_CR40","unstructured":"Yu, G., Bae, K.: Maude-SE: a tight integration of Maude and SMT solvers. In: Proceedings of International Workshop on Rewriting Logic and its Applications (2020)"},{"key":"665_CR41","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Proceedings of TACAS, vol. 9035. LNCS, Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-46681-0_4"},{"key":"665_CR42","doi-asserted-by":"crossref","unstructured":"Frehse, G., Guernic, C.L., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Proceedings of CAV, vol. 6806. LNCS, Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"665_CR43","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Proceedings of CAV, pp. 258\u2013263 (2013). Springer","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"665_CR44","doi-asserted-by":"crossref","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.M.: dReach: $$\\delta $$-reachability analysis for hybrid systems. In: Proceedings of TACAS, vol. 7898, pp. 200\u2013205. LNCS, Springer, Berlin (2015)","DOI":"10.1007\/978-3-662-46681-0_15"},{"key":"665_CR45","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: Proceedings of HSCC\u201915, pp. 128\u2013133 (2015)","DOI":"10.1145\/2728606.2728630"},{"key":"665_CR46","doi-asserted-by":"crossref","unstructured":"Ahmad, E., Dong, Y., Wang, S., Zhan, N., Zou, L.: Adding formal meanings to AADL with Hybrid Annex. In: Proceedings of FACS, vol. 8997. LNCS, Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-15317-9_15"},{"issue":"12","key":"665_CR47","doi-asserted-by":"publisher","first-page":"1989","DOI":"10.1109\/TCAD.2017.2681076","volume":"36","author":"Y Bao","year":"2017","unstructured":"Bao, Y., Chen, M., Zhu, Q., Wei, T., Mallet, F., Zhou, T.: Quantitative performance evaluation of uncertainty-aware Hybrid AADL designs using statistical model checking. IEEE Trans. CAD Integr. Circuits Syst. 36(12), 1989\u20132002 (2017)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"issue":"3","key":"665_CR48","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/s11704-018-7039-7","volume":"13","author":"J Liu","year":"2019","unstructured":"Liu, J., Li, T., Ding, Z., Qian, Y., Sun, H., He, J.: AADL+: a simulation-based methodology for cyber-physical systems. Front. Comput. Sci. 13(3), 516\u2013538 (2019)","journal-title":"Front. Comput. Sci."},{"key":"665_CR49","doi-asserted-by":"crossref","unstructured":"Bae, K., \u00d6lveczky, P.C., Meseguer, J., Al-Nayeem, A.: The SynchAADL2Maude tool. In: Proceedings of FASE\u201912, vol. 7212. LNCS, Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28872-2_4"},{"key":"665_CR50","doi-asserted-by":"crossref","unstructured":"Baudart, G., Bourke, T., Pouzet, M.: Soundness of the quasi-synchronous abstraction. In: Proceedings of FMCAD, pp. 9\u201316 (2016). IEEE","DOI":"10.1109\/FMCAD.2016.7886655"},{"key":"665_CR51","doi-asserted-by":"crossref","unstructured":"Larrieu, R., Shankar, N.: A framework for high-assurance quasi-synchronous systems. In: Proceedings of MEMOCODE, pp. 72\u201383 (2014). IEEE","DOI":"10.1109\/MEMCOD.2014.6961845"},{"key":"665_CR52","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Mandel, L.: Simulation and verification of asynchronous systems by means of a synchronous model. In: Sixth International Conference on Application of Concurrency to System Design (ACSD\u201906), pp. 3\u201314 (2006). IEEE","DOI":"10.1109\/ACSD.2006.24"},{"key":"665_CR53","doi-asserted-by":"crossref","unstructured":"Girault, A., M\u00e9nier, C.: Automatic production of globally asynchronous locally synchronous systems. In: International Workshop on Embedded Software, pp. 266\u2013281 (2002). Springer","DOI":"10.1007\/3-540-45828-X_20"},{"issue":"1","key":"665_CR54","first-page":"131","volume":"78","author":"D Potop-Butucaru","year":"2007","unstructured":"Potop-Butucaru, D., Caillaud, B.: Correct-by-construction asynchronous implementation of modular synchronous specifications. Fund. Inform. 78(1), 131\u2013159 (2007)","journal-title":"Fund. Inform."},{"key":"665_CR55","doi-asserted-by":"crossref","unstructured":"Desai, A., Seshia, S.A., Qadeer, S., Broman, D., Eidson, J.C.: Approximate synchrony: an abstraction for distributed almost-synchronous systems. In: Proceedings of CAV\u201915. LNCS, vol. 9207, pp. 429\u2013448. Springer, Berlin (2015)","DOI":"10.1007\/978-3-319-21668-3_25"},{"key":"665_CR56","doi-asserted-by":"crossref","unstructured":"Bak, S., Duggirala, P.S.: Hylaa: a tool for computing simulation-equivalent reachability for linear systems. In: Proceedings of HSCC, pp. 173\u2013178 (2017)","DOI":"10.1145\/3049797.3049808"},{"key":"665_CR57","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, vol. 3253, pp. 152\u2013166. LNCS, Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"665_CR58","doi-asserted-by":"crossref","unstructured":"Bae, K., Lee, J.: Bounded model checking of signal temporal logic properties using syntactic separation. In: Proceedings of ACM Programming Language, vol. 3 (POPL) (Proceedings of POPL 2019) (2019)","DOI":"10.1145\/3290364"},{"key":"665_CR59","doi-asserted-by":"crossref","unstructured":"Lee, J., Yu, G., Bae, K.: Efficient SMT-based model checking for signal temporal logic. In: Proceedings of 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE\u201921), pp. 343\u2013354 (2021). IEEE","DOI":"10.1109\/ASE51524.2021.9678719"},{"issue":"1","key":"665_CR60","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6\u20131639 (2018)","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"665_CR61","doi-asserted-by":"crossref","unstructured":"AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Proceedings of CALCO 2011, vol. 6859, pp. 386\u2013392. LNCS, Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22944-2_28"},{"issue":"2","key":"665_CR62","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"GA Agha","year":"2006","unstructured":"Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. Electron. Notes Theor. Comput. Sci. 153(2), 213\u2013239 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00665-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-022-00665-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-022-00665-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,3]],"date-time":"2024-10-03T05:26:59Z","timestamp":1727933219000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-022-00665-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,3]]},"references-count":62,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["665"],"URL":"https:\/\/doi.org\/10.1007\/s10009-022-00665-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,9,3]]},"assertion":[{"value":"28 June 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 September 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}