{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T07:11:09Z","timestamp":1726125069831},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2004,6,1]],"date-time":"2004-06-01T00:00:00Z","timestamp":1086048000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Des Autom Embed Syst"],"published-print":{"date-parts":[[2004,6]]},"DOI":"10.1007\/s10617-005-1184-6","type":"journal-article","created":{"date-parts":[[2005,7,15]],"date-time":"2005-07-15T07:14:53Z","timestamp":1121411693000},"page":"67-99","source":"Crossref","is-referenced-by-count":4,"title":["Embedded System Design Using Formal Model Refinement: An Approach Based on the Combined Use of UML and the B Language"],"prefix":"10.1007","volume":"9","author":[{"given":"Nikolaos S.","family":"Voros","sequence":"first","affiliation":[]},{"given":"Colin F.","family":"Snook","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Hallerstede","sequence":"additional","affiliation":[]},{"given":"Konstantinos","family":"Masselos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,7,14]]},"reference":[{"key":"1184_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J. R. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"1184_CR2","unstructured":"Abrial, J. R. Event Driven Electronic Circuit Construction, Available at: http:\/\/www.atelierb.societe.com\/ressources\/articles\/cir.pdf."},{"key":"1184_CR3","unstructured":"Abrial, J. R. Event Model Decomposition, 2004, Available at: http:\/\/www.atelierb.societe.com\/resources\/articles\/dcmp3.pdf."},{"key":"1184_CR4","unstructured":"Boulanger, J. L., and G. Mariano. Formalization of Digital Circuits Using the B Method. In Proceedings of 3rd European Systems Engineering Conference, 2002, pp. 281\u2013290."},{"key":"1184_CR5","unstructured":"B-Toolkit, \u2018B-Toolkit User\u2019s Manual,\u2019 1996, release 3.2, B-Core Ltd, Oxford, United Kingdom."},{"key":"1184_CR6","unstructured":"ClearSy, Event B Reference Manual, 2001, version 1.0, Available at: http:\/\/www.atelierb.societe.com\/ressources\/evt2b\/eventb_reference_manu-al.pdf."},{"key":"1184_CR7","unstructured":"ClearSy: 2004, ClearSy System Engineering: AtelierB User Manual, version 3.6."},{"issue":"2","key":"1184_CR8","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1109\/32.345825","volume":"l21","author":"D. Craigen","year":"1995","unstructured":"Craigen, D., S. Gerhart, and E. Ralston. Formal Methods Reality Check: Industrial Usage. IEEE Transactions on Software Engineering, vol. l21, no. 2, pp. 90\u201398, 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1184_CR9","unstructured":"Draper, J., et al. Evaluating the B Method on an Avionics Example. In Proceedings of Data Systems in Aerospace (DASIA) Conference, 1996, pp. 89\u201397."},{"key":"1184_CR10","unstructured":"Eclipse: 2004, Available at: http:\/\/www.eclipse.org\/."},{"key":"1184_CR11","unstructured":"ETSI: 2000, Broadband Radio Access Networks BRAN; HIPERLAN Type 2; Data Link Control (DLC) Layer Part1: Basic Data Transport Functions, Technical Report ETSI TS 101 761-1 version 1.1.1."},{"key":"1184_CR12","unstructured":"Facon, P., R. Lelau, and H. P. Nguyen. Combining UML with the B Formal Method for the Specification of Database Applications. Research Report, CEDRIC Laboratory, Paris. 1999."},{"key":"1184_CR13","doi-asserted-by":"crossref","unstructured":"Harel, D. StateCharts: A Visual Formalism for Complex Systems. Science of Computer Programming Archive, vol. 8, issue 3, pp. 231\u2013274, 1987.","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"1184_CR14","unstructured":"IBM Rational software: 2004, Available at: http:\/\/www.rational.com\/."},{"key":"1184_CR15","doi-asserted-by":"crossref","unstructured":"Ifill, W., et al., The use of B to Specify, Design and Verify Hardware in High Integrity Software, High Integrity Software, Kluwer Academic Publishers, 2002, pp. 43\u201362.","DOI":"10.1007\/978-1-4615-1391-9_3"},{"key":"1184_CR16","unstructured":"KeesDA: BHDL User Guide, 2004, Available At: http:\/\/www.keesda.com\/pussee\/bibliography.htm."},{"key":"1184_CR17","doi-asserted-by":"crossref","unstructured":"Lano, K., D. Clark, and K. Androutsopoulos, UML to B: Formal Verification of Object-Oriented Models, In E. A. Boiten, J.Derrick, G.Smith (Eds.), Integrated Formal Methods, 4th International Conference, IFM 2004, Lecture Notes in Computer Science, 2004, vol. 2999, pp. 187\u2013206.","DOI":"10.1007\/978-3-540-24756-2_11"},{"key":"1184_CR18","unstructured":"Lecomte, T., J. R. Abrial, F. Badeau, C. Czernecki, D. Sabatier, and C. Snook, Abstract Modeling: System Level Modeling and Refinement in B, Technical Report, Project IST-2000-30103 PUSSEE, 2004, Available at: http:\/\/www.keesda.com\/pussee."},{"key":"1184_CR19","unstructured":"Ledang, H., and J. Souquieres, Integrating UML and B Specification Techniques. Proceedings of Informatik 2001 Workshop on Integrating Diagrammatic and Formal SpecificationTechnique, 2001, pp. 53\u201360."},{"key":"1184_CR20","unstructured":"Rumbaugh, J., I. Jacobson, and G. Booch. The Unified modeling Language Reference Manual. Addison-Wesley, 1998."},{"key":"1184_CR21","doi-asserted-by":"crossref","unstructured":"Sekerinski, E. Graphical Design of Reactive Systems, In D. Bert (Ed.), B\u201998\u2014Recent Advances in the Development and Use of the B Method, Lecture Notes in Computer Science 1393. Springer-Verlag, pp. 182\u2013197, 1998.","DOI":"10.1007\/BFb0053361"},{"key":"1184_CR22","unstructured":"Snook, C., and M. Butler, Final Tool Extensions for Integration of UML and B, Technical Report D4.1.3, Project IST-2000-30103 PUSSEE, 2004, Available at: http:\/\/www.keesda.com\/pussee."},{"key":"1184_CR23","unstructured":"Snook, C., L. Tsiopoulos, and M. Walden, A Case Study in Requirement Analysis of Control Systems using UML and B. In Proceedings of International Workshop on Refinement of Critical Systems, Methods, Tools and Developments, 2003, Available at: http:\/\/www.esil.univ-mrs.fr\/spc\/rcs03\/rcs03.html."},{"key":"1184_CR24","unstructured":"The PUSSEE Project: 2004, Available at: http:\/\/www.keesda.com\/pussee."},{"key":"1184_CR25","unstructured":"Warmer, J., and A. Kleppe, The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, 1999."},{"key":"1184_CR26","unstructured":"XMI: 2004, Available at: http:\/\/www.omg.org\/technology\/documents\/formal\/xmi.htm."}],"container-title":["Design Automation for Embedded Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10617-005-1184-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10617-005-1184-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10617-005-1184-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T07:31:58Z","timestamp":1586331118000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10617-005-1184-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,6]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,6]]}},"alternative-id":["1184"],"URL":"https:\/\/doi.org\/10.1007\/s10617-005-1184-6","relation":{},"ISSN":["0929-5585","1572-8080"],"issn-type":[{"value":"0929-5585","type":"print"},{"value":"1572-8080","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,6]]}}}