{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T16:10:07Z","timestamp":1746375007318,"version":"3.40.4"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319108810"},{"type":"electronic","value":"9783319108827"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10882-7_2","type":"book-chapter","created":{"date-parts":[[2014,9,11]],"date-time":"2014-09-11T06:54:19Z","timestamp":1410418459000},"page":"17-24","source":"Crossref","is-referenced-by-count":1,"title":["Event Analytics"],"prefix":"10.1007","author":[{"given":"Jin Song","family":"Dong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan-Fang","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"[Ang87] Angluin, D.: Learning Regular Sets from Queries and Counterexamples. Information and Computation\u00a075(2), 87\u2013106 (1987)","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"[BCLR04] Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 1\u201320. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"2_CR3","unstructured":"[BLM+13] Bai, G., Lei, J., Meng, G., Venkatraman, S., Saxena, P., Sun, J., Liu, Y., Dong, J.S.: AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 2013, San Diego, USA (2013)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"[BMD10] Biswas, J., Mokhtari, M., Dong, J.S., Yap, P.: Mild dementia care at home \u2013 integrating activity monitoring, user interface plasticity and scenario verification. In: Lee, Y., Bien, Z.Z., Mokhtari, M., Kim, J.T., Park, M., Kim, J., Lee, H., Khalil, I. (eds.) ICOST 2010. LNCS, vol.\u00a06159, pp. 160\u2013170. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-13778-5_20"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"[BCM+92] Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and computation\u00a098(2), 142\u2013170 (1992)","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"[BSH13] Barnaghi, P., Sheth, A., Henson, C.: From Data to Actionable Knowledge: Big Data Challenges in the Web of Things. IEEE Intelligent Systems (November\/December 2013)","DOI":"10.1109\/MIS.2013.142"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"[CZ13] Ciobanu, G., Zheng, M.: Automatic Analysis of TiMo Systems in PAT. In: Engineering of Complex Computer Systems, ICECCS (2013)","DOI":"10.1109\/ICECCS.2013.25"},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"[CE81] Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logic of Programs, 52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"[DeB] de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"[DSL13] Dong, J.S., Sun, J., Liu, Y.: Build Your Own Model Checker in One Month. In: 35th International Conference on Software Engineering (ICSE 2013, tutorial), San Francisco, CA, USA, May18-26 (2013)","DOI":"10.1109\/ICSE.2013.6606751"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"[GSL+13] Gui, L., Sun, J., Liu, Y., Si, Y., Dong, J.S., Wang, X.: Combining Model Checking and Testing with an Application to Reliability Prediction and Distribution. In: ISSTA 2013, Lugano, Switzerland, July 15-20 (2013)","DOI":"10.1145\/2483760.2483779"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"[HSL+12] Hao, J., Song, S., Liu, Y., Sun, J., Gui, L., Dong, J.S., Leung, H.-F.: Probabilistic Model Checking Multi-agent Behaviors in Dispersion Games Using Counter Abstraction. In: Rahwan, I., Wobcke, W., Sen, S., Sugawara, T. (eds.) PRIMA 2012. LNCS, vol.\u00a07455, pp. 16\u201330. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-32729-2_2"},{"key":"2_CR13","unstructured":"[Hoare85] Hoare, C.A.R.: Communicating Sequential Process. Prentice Hall (1985)"},{"key":"2_CR14","unstructured":"[HH98] Hoare, C.A.R., He, J.: Unifying Theory of Programming. Pretice Hall (1998)"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"[KGN+09] Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodov\u00e1, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing Testing with Formal Verification in Intel\u00ae CoreTM i7 Processor Execution Engine Validation. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 414\u2013429. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02658-4_32"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"[LAL+14] Lin, S.-W., Andr\u00e9, \u00c9., Liu, Y., Sun, J., Dong, J.S.: Learning Assumptions for Compositional Verification of Timed Systems. IEEE Trans. Software Eng.\u00a040(2), 137\u2013153 (2014)","DOI":"10.1109\/TSE.2013.57"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"[LCL+13] Liu, Y., Chen, W., Liu, Y.A., Sun, J., Zhang, S., Dong, J.S.: Verifying Linearizability via Optimized Refinement Checking. IEEE Transactions on Software Engineering\u00a039(7), 1018\u20131039 (2013)","DOI":"10.1109\/TSE.2012.82"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"[LLX02] Lee, V.Y., Liu, Y., Zhang, X., Phua, C., Sim, K., Zhu, J., Biswas, J., Dong, J.S., Mokhtari, M.: ACARP: Auto correct activity recognition rules using process analysis toolkit (PAT). In: Donnelly, M., Paggetti, C., Nugent, C., Mokhtari, M. (eds.) ICOST 2012. LNCS, vol.\u00a07251, pp. 182\u2013189. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-30779-9_23"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"[LDS+14] Li, Y., Dong, J.S., Sun, J., Liu, Y., Sun, J.: Model Checking Approach to Automated Planning. Formal Methods in System Design\u00a044(2), 176\u2013202 (2014)","DOI":"10.1007\/s10703-013-0197-1"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"[Len02] Lenzerini, M.: Data integration: A theoretical perspective. In: Proceedings of the Twenty-first ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS). ACM (2002)","DOI":"10.1145\/543643.543644"},{"key":"2_CR21","unstructured":"[LYW11] Li, Y., Yang, H., Wu, H.: PAT Approach to Transport4You, an intelligent public transportation manager (Tutors: J. S. Dong, Y. Liu, J. Sun), ICSE 2011 SCORE winner. 94 teams from 22 countries registered the competition where 56 teams completed the projects; two teams were selected as winners."},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"[MD00] Mahony, B., Dong, J.S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering\u00a026(2), 150\u2013177 (2000)","DOI":"10.1109\/32.841115"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"[MWC10] Miller, S.P., Whalen, M.W., Cofer, D.D.: Software model checking takes off. Commun. ACM\u00a053(2), 58\u201364 (2010)","DOI":"10.1145\/1646353.1646372"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"[SZL+13] Shi, L., Zhao, Y., Liu, Y., Sun, J., Dong, J.S., Qin, S.: A UTP Semantics for Communicating Processes with Shared Variables. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol.\u00a08144, pp. 215\u2013230. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-41202-8_15"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"[SD06] Sun, J., Dong, J.S.: Design Synthesis from Interaction and State-based Specifications. IEEE Transactions on Software Engineering (TSE)\u00a032(6), 349\u2013364 (2006)","DOI":"10.1109\/TSE.2006.55"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"[SLDP09] Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"[SSLD12] Song, S., Sun, J., Liu, Y., Dong, J.S.: A Model Checker for Hierarchical Probabilistic Real-Time Systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 705\u2013711. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-31424-7_53"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"[SYD+13] Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Andr\u00e9, \u00c9.: Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP. The ACM Transactions on Software Engineering and Methodology (TOSEM)\u00a022(1), 3:1-3:29 (2013)","DOI":"10.1145\/2430536.2430537"},{"key":"2_CR29","doi-asserted-by":"crossref","unstructured":"[TDC04] Taguchi, K., Dong, J.S., Ciobanu, G.: Relating Pi-calculus to Object-Z. In: The 9th IEEE International Conference on Engineering Complex Computer Systems (ICECCS 2004), Florence, Italy, pp. 97\u2013106. IEEE Press (2004)","DOI":"10.1109\/ICECCS.2004.1310908"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"[TAS+13] Tan, T.H., Andre, E., Sun, J., Liu, Y., Dong, J.S., Chen, M.: Dynamic Synthesis of Local Time Requirement for Service Composition. In: ICSE 2013 (2013)","DOI":"10.1109\/ICSE.2013.6606600"},{"key":"2_CR31","unstructured":"[WD96] Woodcock, J., Davies, J.: Using Z: specification, refinement, and proof. Prentice-Hall (1996)"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"[WSC+08] Woodcock, J., Stepney, S., Cooper, D., Clark, J.A., Jacob, J.: The certification of the Mondex electronic purse to ITSEC Level E6. Formal Asp. Comput.\u00a020(1), 5\u201319 (2008)","DOI":"10.1007\/s00165-007-0060-5"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"[ZSS+13] Zheng, M., San\u00e1n, D., Sun, J., Liu, Y., Dong, J.S., Gu, Y.: State Space Reduction for Sensor Networks using Two-level Partial Order Reduction. In: The 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2013), Rome, Italy, pp. 515\u2013535 (January 2013)","DOI":"10.1007\/978-3-642-35873-9_30"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10882-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T15:44:35Z","timestamp":1746373475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10882-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319108810","9783319108827"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10882-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}