{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:29:19Z","timestamp":1742387359881,"version":"3.37.3"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,8,14]],"date-time":"2017-08-14T00:00:00Z","timestamp":1502668800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Funda\u00e7\u00e3o de Amparo a Pesquisa de Alagoas"},{"DOI":"10.13039\/501100002322","name":"Coordena\u00e7\u00e3o de Aperfei\u00e7oamento de Pessoal de N\u00edvel Superior","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002322","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003593","name":"Conselho Nacional de Desenvolvimento Cient\u00edfico e Tecnol\u00f3gico","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2019,4]]},"DOI":"10.1007\/s10270-017-0616-7","type":"journal-article","created":{"date-parts":[[2017,8,14]],"date-time":"2017-08-14T02:35:54Z","timestamp":1502678154000},"page":"1467-1485","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal modeling of biomedical signal acquisition systems: source of evidence for certification"],"prefix":"10.1007","volume":"18","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8934-5309","authenticated-orcid":false,"given":"Alvaro","family":"Sobrinho","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leandro Dias","family":"da Silva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Perkusich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paulo","family":"Cunha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thiago","family":"Cordeiro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonio Marcus Nogueira","family":"Lima","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,14]]},"reference":[{"issue":"4","key":"616_CR1","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/MSP.2013.49","volume":"11","author":"H Alemzadeh","year":"2013","unstructured":"Alemzadeh, H., Iyer, R., Kalbarczyk, Z., Raman, J.: Analysis of safety-critical computer failures in medical devices. IEEE Secur. Priv. 11(4), 14\u201326 (2013)","journal-title":"IEEE Secur. Priv."},{"key":"616_CR2","unstructured":"Analog Devices: Single-Lead, Heart Rate Monitor Front End Data Sheet AD8232 (2013)"},{"key":"616_CR3","unstructured":"Analog Devices: Low Power, Precision Analog Microcontroller with Dual Sigma-Delta ADCs, ARM Cortex-M3, Data Sheet ADuCM360\/ADuCM361 (2014)"},{"key":"616_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: Joint Workshop on High Confidence Medical Devices, Software, and Systems and Medical Device Plug-and-Play Interoperability, pp. 23\u201333 (2007)","DOI":"10.1109\/HCMDSS-MDPnP.2007.36"},{"key":"616_CR5","doi-asserted-by":"crossref","unstructured":"Barbosa, P., Morais, M., Galdino, K., Andrade, M., Gomes, L., Moutinho, F., de\u00a0Figueiredo, J.: Towards medical device behavioural validation using petri nets. In: IEEE 26th International Symposium on Computer-Based Medical Systems (CBMS), pp. 4\u201310 (2013)","DOI":"10.1109\/CBMS.2013.6627756"},{"issue":"3","key":"616_CR6","first-page":"1354","volume":"2","author":"B Chandrakar","year":"2013","unstructured":"Chandrakar, B., Yadav, O., Chandra, V.: A survey of noise removal techniques for ecg signals. Int. J. Adv. Res. Comput. Commun. Eng. 2(3), 1354\u20131357 (2013)","journal-title":"Int. J. Adv. Res. Comput. Commun. Eng."},{"issue":"5","key":"616_CR7","first-page":"340","volume":"4","author":"MS Chavan","year":"2008","unstructured":"Chavan, M.S., Agarwala, R.A., Uplane, M.D.: Interference reduction in ecg using digital fir filters based on rectangular window. WSEAS Trans. Signal Process. 4(5), 340\u2013349 (2008)","journal-title":"WSEAS Trans. Signal Process."},{"key":"616_CR8","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge, MA (1999)"},{"issue":"2","key":"616_CR9","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1007\/s10270-014-0423-3","volume":"14","author":"J Desel","year":"2014","unstructured":"Desel, J., Reisig, W.: The concepts of petri nets. Softw. Syst. Model. 14(2), 669\u2013683 (2014)","journal-title":"Softw. Syst. Model."},{"key":"616_CR10","unstructured":"FDA: Medical device classification procedures (Revised as of April 2016)"},{"issue":"101","key":"616_CR11","first-page":"215","volume":"23","author":"A Goldberger","year":"2000","unstructured":"Goldberger, A., Amaral, L., Glass, L., Hausdorff, J.M., Ivanov, P.C., Mark, R., Mietus, J., Moody, G., Peng, C.K., Stanley, H.: Physiobank, physiotoolkit, and physionet: components of a new research resource for complex physiologic signals. Circulation 23(101), 215\u2013220 (2000)","journal-title":"Circulation"},{"issue":"7","key":"616_CR12","doi-asserted-by":"publisher","first-page":"4267","DOI":"10.1109\/TIE.2014.2387337","volume":"62","author":"J Han","year":"2015","unstructured":"Han, J., Ding, Q., Xiong, A., Zhao, X.: A state-space emg model for the estimation of continuous joint movements. IEEE Trans. Industr. Electron. 62(7), 4267\u20134275 (2015)","journal-title":"IEEE Trans. Industr. Electron."},{"key":"616_CR13","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/j.ssci.2013.04.007","volume":"59","author":"R Hawkins","year":"2013","unstructured":"Hawkins, R., Habli, I., Kelly, T., McDermid, J.: Assurance cases and prescriptive software safety certification: a comparative study. Saf. Sci. 59, 55\u201371 (2013)","journal-title":"Saf. Sci."},{"key":"616_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/b95112","volume-title":"Coloured Petri Nets: Modelling and Validation of Concurrent Systems","author":"K Jensen","year":"2009","unstructured":"Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems, 1st edn. Springer, Berlin (2009)","edition":"1"},{"issue":"6","key":"616_CR15","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/2663340","volume":"58","author":"K Jensen","year":"2015","unstructured":"Jensen, K., Kristensen, L.M.: Colored petri nets: a graphical language for formal modeling and validation of concurrent systems. Commun. ACM 58(6), 61\u201370 (2015)","journal-title":"Commun. ACM"},{"issue":"3","key":"616_CR16","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/s10009-007-0038-x","volume":"9","author":"K Jensen","year":"2007","unstructured":"Jensen, K., Kristensen, L.M., Wells, L.: Coloured petri nets and cpn tools for modelling and validation of concurrent systems. Int. J. Softw. Tools Technol. Transfer 9(3), 213\u2013254 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"2","key":"616_CR17","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10009-013-0289-7","volume":"16","author":"Z Jiang","year":"2014","unstructured":"Jiang, Z., Pajic, M., Alur, R., Mangharam, R.: Closed-loop verification of medical devices with model abstraction and refinement. Int. J. Softw. Tools Technol. Transfer 16(2), 191\u2013213 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"1","key":"616_CR18","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1109\/JPROC.2011.2161241","volume":"100","author":"Z Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Mangharam, R.: Cyber-physical modeling of implantable cardiac medical devices. Proc. IEEE 100(1), 122\u2013137 (2012)","journal-title":"Proc. IEEE"},{"key":"616_CR19","doi-asserted-by":"crossref","unstructured":"Kim, B., Ayoub, A., Sokolsky, O., Lee, I., Jones, P., Zhang, Y., Jetley, R.: Safety-assured development of the gpca infusion pump software. In: Proceedings of the Ninth ACM International Conference on Embedded Software, EMSOFT \u201911, pp. 155\u2013164 (2011)","DOI":"10.1145\/2038642.2038667"},{"issue":"2","key":"616_CR20","doi-asserted-by":"publisher","first-page":"839","DOI":"10.1007\/s10270-013-0342-8","volume":"14","author":"J Kim","year":"2013","unstructured":"Kim, J., Kang, I., Choi, J., Lee, I., Kang, S.: Formal synthesis of application and platform behaviors of embedded software systems. Softw. Syst. Model. 14(2), 839\u2013859 (2013)","journal-title":"Softw. Syst. Model."},{"key":"616_CR21","unstructured":"Kitchin, C., Counts, L.: A designer\u2019s guide to instrumentation amplifiers, 3th edn. Analog Devices (2006)"},{"issue":"10","key":"616_CR22","doi-asserted-by":"publisher","first-page":"1306","DOI":"10.1161\/CIRCULATIONAHA.106.180200","volume":"115","author":"P Kligfield","year":"2007","unstructured":"Kligfield, P., Gettes, L.S., Bailey, J.J., Childers, R., Deal, B.J., Hancock, E.W., van Herpen, G., Kors, J.A., Macfarlane, P., Mirvis, D.M., Pahlm, O., Rautaharju, P., Wagner, G.S.: Recommendations for the standardization and interpretation of the electrocardiogram: Part I: the electrocardiogram and its technology: a scientific statement from the american heart association electrocardiography and arrhythmias committee, council on clinical cardiology; the american college of cardiology foundation; and the heart rhythm society endorsed by the international society for computerized electrocardiology. Circulation 115(10), 1306\u20131324 (2007)","journal-title":"Circulation"},{"issue":"3","key":"616_CR23","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1109\/TII.2010.2050001","volume":"6","author":"M Kloetzer","year":"2010","unstructured":"Kloetzer, M., Mahulea, C., Belta, C., Silva, M.: An automated framework for formal verification of timed continuous petri nets. IEEE Trans. Ind. Inf. 6(3), 460\u2013471 (2010)","journal-title":"IEEE Trans. Ind. Inf."},{"issue":"2","key":"616_CR24","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/s10270-014-0421-5","volume":"14","author":"I Koch","year":"2014","unstructured":"Koch, I.: Petri nets in systems biology. Softw. Syst. Model. 14(2), 703\u2013710 (2014)","journal-title":"Softw. Syst. Model."},{"issue":"4","key":"616_CR25","doi-asserted-by":"publisher","first-page":"2364","DOI":"10.1109\/TPWRS.2011.2118772","volume":"26","author":"YS Lee","year":"2011","unstructured":"Lee, Y.S., Kim, D.J., Kim, J.O., Kim, H.: New fmeca methodology using structural importance and fuzzy theory. IEEE Trans. Power Syst. 26(4), 2364\u20132370 (2011)","journal-title":"IEEE Trans. Power Syst."},{"issue":"3","key":"616_CR26","doi-asserted-by":"publisher","first-page":"1764","DOI":"10.1109\/TII.2013.2245334","volume":"9","author":"S Li","year":"2013","unstructured":"Li, S., Xu, L.D., Wang, X.: A continuous biomedical signal acquisition system based on compressed sensing in body sensor networks. IEEE Trans. Ind. Inf. 9(3), 1764\u20131771 (2013)","journal-title":"IEEE Trans. Ind. Inf."},{"issue":"3","key":"616_CR27","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1109\/TPDS.2013.50","volume":"25","author":"T Li","year":"2014","unstructured":"Li, T., Tan, F., Wang, Q., Bu, L., Cao, J., Liu, X.: From offline toward real time: a hybrid systems model checking and cps codesign approach for medical device plug-and-play collaborations. IEEE Trans. Parallel Distrib. Syst. 25(3), 642\u2013652 (2014)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"616_CR28","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-10509-3_10","volume-title":"Computer and Information Science, Studies in Computational Intelligence","author":"CL Lin","year":"2015","unstructured":"Lin, C.L., Shen, W.: Generation of assurance cases for medical devices. In: Lee, R. (ed.) Computer and Information Science, Studies in Computational Intelligence, vol. 566, pp. 127\u2013140. Springer, Berlin (2015)"},{"issue":"3","key":"616_CR29","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/s11219-015-9288-0","volume":"24","author":"A Mashkoor","year":"2016","unstructured":"Mashkoor, A.: Model-driven development of high-assurance active medical devices. Soft. Qual. J. 24(3), 571\u2013596 (2016)","journal-title":"Soft. Qual. J."},{"issue":"1","key":"616_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2406336.2406351","volume":"12","author":"D M\u00e9ry","year":"2013","unstructured":"M\u00e9ry, D., Singh, N.K.: Formal specification of medical systems by proof-based refinement. ACM Trans. Embed. Comput. Syst. 12(1), 1\u201325 (2013)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"616_CR31","doi-asserted-by":"crossref","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised), 1th edn. MIT Press (1997)","DOI":"10.7551\/mitpress\/2319.001.0001"},{"issue":"2","key":"616_CR32","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1109\/TCSII.2015.2483377","volume":"63","author":"P Mitros","year":"2016","unstructured":"Mitros, P.: Filters with decreased passband error. IEEE Trans. Circuits Syst. II Express Br. 63(2), 131\u2013135 (2016)","journal-title":"IEEE Trans. Circuits Syst. II Express Br."},{"issue":"4","key":"616_CR33","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"issue":"1","key":"616_CR34","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/TII.2012.2226594","volume":"10","author":"M Pajic","year":"2014","unstructured":"Pajic, M., Mangharam, R., Sokolsky, O., Arney, D., Goldman, J., Lee, I.: Model-driven safety analysis of closed-loop medical systems. IEEE Trans. Ind. Inf. 10(1), 3\u201316 (2014)","journal-title":"IEEE Trans. Ind. Inf."},{"key":"616_CR35","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-8888-8","volume-title":"Analog-to-Digital Conversion","author":"M Pelgrom","year":"2010","unstructured":"Pelgrom, M.: Analog-to-Digital Conversion, 1st edn. Springer, Netherlands (2010)","edition":"1"},{"issue":"1","key":"616_CR36","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1109\/COMST.2014.2345792","volume":"17","author":"J Qadir","year":"2015","unstructured":"Qadir, J., Hasan, O.: Applying formal methods to networking: theory, techniques, and applications. IEEE Commun. Surv. Tutor. 17(1), 256\u2013291 (2015)","journal-title":"IEEE Commun. Surv. Tutor."},{"key":"616_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-6629-0","volume-title":"Fast Fourier Transform\u2014Algorithms and Applications","author":"KR Rao","year":"2010","unstructured":"Rao, K.R., Kim, D.N., Hwang, J.J.: Fast Fourier Transform\u2014Algorithms and Applications, 1st edn. Springer, Netherlands (2010)","edition":"1"},{"key":"616_CR38","doi-asserted-by":"publisher","first-page":"1676","DOI":"10.1109\/ACCESS.2016.2548362","volume":"4","author":"N Razzaq","year":"2016","unstructured":"Razzaq, N., Sheikh, S.A.A., Salman, M., Zaidi, T.: An intelligent adaptive filter for elimination of power line interference from high resolution electrocardiogram. IEEE Access 4, 1676\u20131688 (2016)","journal-title":"IEEE Access"},{"issue":"3","key":"616_CR39","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1109\/TSTE.2013.2241797","volume":"4","author":"M Schlechtingen","year":"2013","unstructured":"Schlechtingen, M., Santos, I.F., Achiche, S.: Using data-mining approaches for wind turbine power curve monitoring: a comparative study. IEEE Trans. Sustain. Energy 4(3), 671\u2013679 (2013)","journal-title":"IEEE Trans. Sustain. Energy"},{"key":"616_CR40","volume-title":"Microelectronic Circuits","author":"AS Sedra","year":"2009","unstructured":"Sedra, A.S., Smith, K.C.: Microelectronic Circuits, 6th edn. Oxford University Press, Oxford (2009)","edition":"6"},{"issue":"3","key":"616_CR41","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10207-014-0243-z","volume":"14","author":"Y Seifi","year":"2015","unstructured":"Seifi, Y., Suriadi, S., Foo, E., Boyd, C.: Analysis of two authorization protocols using colored petri nets. Int. J. Inf. Secur. 14(3), 221\u2013247 (2015)","journal-title":"Int. J. Inf. Secur."},{"issue":"11","key":"616_CR42","doi-asserted-by":"publisher","first-page":"27625","DOI":"10.3390\/s151127625","volume":"15","author":"LC Silva","year":"2015","unstructured":"Silva, L.C., Almeida, H.O., Perkusich, A., Perkusich, M.: A model-based approach to support validation of medical cyber-physical systems. Sensors 15(11), 27625\u201327670 (2015)","journal-title":"Sensors"},{"key":"616_CR43","doi-asserted-by":"crossref","unstructured":"Sobrinho, A., Perkusich, A., Dias\u00a0da Silva, L., Cordeiro, T., Rego, J., Cunha, P.: Towards medical device certification: a colored petri nets model of a surface electrocardiography device. In: 40th Annual Conference of the IEEE Industrial Electronics Society, pp. 2645\u20132651 (2014)","DOI":"10.1109\/IECON.2014.7048879"},{"key":"616_CR44","doi-asserted-by":"crossref","unstructured":"Sobrinho, A., Perkusich, A., Dias\u00a0da Silva, L., Cunha, P.: Using colored petri nets for the requirements engineering of a surface electrogastrography system. In: IEEE International Conference on Industrial Informatics (INDIN), pp. 221\u2013226 (2014)","DOI":"10.1109\/INDIN.2014.6945511"},{"key":"616_CR45","doi-asserted-by":"crossref","unstructured":"Sun, X., Zhang, Y.: Design and implementation of portable ecg and body temperature monitor. In: International Symposium on Computer, Consumer and Control, pp. 188\u2013192 (2014)","DOI":"10.1109\/IS3C.2014.239"},{"key":"616_CR46","doi-asserted-by":"publisher","first-page":"3503","DOI":"10.3233\/BME-141176","volume":"24","author":"TV Tran","year":"2014","unstructured":"Tran, T.V., Chung, W.Y.: IEEE-802.15.4-based low-power body sensor node with RF energy harvester. Bio Med. Mater. Eng. 24, 3503\u20133510 (2014)","journal-title":"Bio Med. Mater. Eng."},{"issue":"2","key":"616_CR47","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/s10270-014-0422-4","volume":"14","author":"K Wolf","year":"2014","unstructured":"Wolf, K.: The petri net twist in explicit model checking. Softw. Syst. Model. 14(2), 711\u2013717 (2014)","journal-title":"Softw. Syst. Model."},{"key":"616_CR48","doi-asserted-by":"publisher","unstructured":"Wu, D., Schnieder, E.: Scenario-based system design with colored petri nets: an application to train control systems. Softw. Syst. Model. 1\u201323 (2016). doi:\n                    10.1007\/s10270-016-0517-1","DOI":"10.1007\/s10270-016-0517-1"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-017-0616-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-017-0616-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-017-0616-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T11:04:15Z","timestamp":1576839855000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-017-0616-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,14]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,4]]}},"alternative-id":["616"],"URL":"https:\/\/doi.org\/10.1007\/s10270-017-0616-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"type":"print","value":"1619-1366"},{"type":"electronic","value":"1619-1374"}],"subject":[],"published":{"date-parts":[[2017,8,14]]},"assertion":[{"value":"16 June 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 April 2017","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 July 2017","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 August 2017","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}