{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:10:08Z","timestamp":1761487808845},"reference-count":39,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["European Journal of Control"],"published-print":{"date-parts":[[2006,1]]},"DOI":"10.3166\/ejc.12.115-130","type":"journal-article","created":{"date-parts":[[2007,3,30]],"date-time":"2007-03-30T16:09:32Z","timestamp":1175270972000},"page":"115-130","source":"Crossref","is-referenced-by-count":7,"title":["Formal Specification Method for Systems Automation"],"prefix":"10.1016","volume":"12","author":[{"given":"Jean-Fran\u00e7ois","family":"P\u00e9tin","sequence":"first","affiliation":[]},{"given":"G\u00e9rard","family":"Morel","sequence":"additional","affiliation":[]},{"given":"Herv\u00e9","family":"Panetto","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.3166\/ejc.12.115-130_bib0005","unstructured":"Abrial JR, Borger E, Langmaack (eds). Formal methods for industrial applications: specifying and programming the steam boiler control. Lecture Notes in Computer Science, State of the art-Survey, ISBN 3-540r-r61929-1."},{"key":"10.3166\/ejc.12.115-130_bib0010","unstructured":"Abrial JR. The B book: assigning programs to meanings. Cambridge University Press, ISBN 0-521r-r49619-5."},{"key":"10.3166\/ejc.12.115-130_bib0015","series-title":"Proceedings of the second international B conference","article-title":"Introducing dynamic constraints in B","author":"Abrial","year":"1998"},{"key":"10.3166\/ejc.12.115-130_bib0020","series-title":"European Systems Engineering Conference","first-page":"21","article-title":"A component based methodology for description of complex systems: an application to avionics systems","author":"Ait-Ameur","year":"2002"},{"key":"10.3166\/ejc.12.115-130_bib0025","series-title":"Construction of finite labelled transition systems from B abstract Systems. Integrated Formal Methods, IFM2000, LNCS 1945","first-page":"235","author":"Bert","year":"2000"},{"key":"10.3166\/ejc.12.115-130_bib0030","series-title":"Proceedings of FME 2003","first-page":"94","article-title":"Adaptable translator of B specifications to embedded C programs","author":"Bert","year":"2003"},{"key":"10.3166\/ejc.12.115-130_bib0035","unstructured":"Cassandras CG, Lafortune S. Introduction to discrete event systems. Kluwer Academic Publisher, ISBN 0-7923r-r8609-4."},{"key":"10.3166\/ejc.12.115-130_bib0040","series-title":"Model checking","author":"Clarke","year":"2000"},{"key":"10.3166\/ejc.12.115-130_bib0045","series-title":"Formal methods technology transfer : implements and innovation, Formal Methods by Hinchey MG","first-page":"399","author":"Craigen","year":"1995"},{"key":"10.3166\/ejc.12.115-130_bib0050","first-page":"2","article-title":"Paraphrasing of specification written in B","volume":"1","author":"Diallo","year":"1998","journal-title":"Networking Inform Syst J"},{"key":"10.3166\/ejc.12.115-130_bib0055","series-title":"Validation of UML models thanks to Z and Lustre","author":"Dupuy","year":"2000"},{"key":"10.3166\/ejc.12.115-130_bib0060","series-title":"IEEE SMC Conference","article-title":"Towards a language of physical systems","author":"F\u00e9 liot","year":"1996"},{"key":"10.3166\/ejc.12.115-130_bib0065","first-page":"6","article-title":"Specification, design, and implementation of logic controllers based on coloured petri net models and the standard IEC 1131","volume":"7","author":"Feldmann","year":"1999","journal-title":"IEEE Trans Control Syst Technol"},{"key":"10.3166\/ejc.12.115-130_bib0070","series-title":"Proceedings of the international joint conference on artificial intelligence","first-page":"405","article-title":"A description and reasoning of plant controllers in temporal logic","author":"Fusaoka","year":"1983"},{"key":"10.3166\/ejc.12.115-130_bib0075","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1017\/S0263574702004824","article-title":"Proactive maintenance strategy for harbour crane operation improvement","volume":"21","author":"Iung","year":"2003","journal-title":"Robotica"},{"key":"10.3166\/ejc.12.115-130_bib0080","series-title":"proceedings of 11th IFAC International Conference on Information Control Problems","article-title":"Improving automation software dependability: a role for formal methods ?","author":"Johnson","year":"2004"},{"key":"10.3166\/ejc.12.115-130_bib0085","series-title":"International conference on formal specification and development in Z and B (ZB2002)","first-page":"517","article-title":"Coming and going from UML to B : a proposal to support traceability in rigorous IS development","author":"Laleau","year":"2002"},{"key":"10.3166\/ejc.12.115-130_bib0090","unstructured":"Lamboley P. Production Systems Automation Formal Method Proposal, PhD Thesis, University Henri Poincar\u00e9, Nancy 1, 2001.(in French)."},{"key":"10.3166\/ejc.12.115-130_bib0095","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0967-0661(99)00138-0","article-title":"Experiences of using formal methods for chemical process control specification","volume":"8","author":"Lano","year":"2000","journal-title":"Control Eng. Practice"},{"key":"10.3166\/ejc.12.115-130_bib0100","isbn-type":"print","author":"Lano","year":"1996","ISBN":"http:\/\/id.crossref.org\/isbn\/3540760334"},{"key":"10.3166\/ejc.12.115-130_bib0105","series-title":"Proceedings of RCS\u201902 international workshop on refinement of critical systems : methods, tools and experience, in conjunction with the 2nd Conference of B and Z Users (ZB 2002), January 23-25","article-title":"language, tool support and experiments","author":"Lecomte","year":"2002"},{"key":"10.3166\/ejc.12.115-130_bib0110","series-title":"proceedings of the International Workshop on refinement of critical systems: methods, tools and experience, in conjunction with the 2nd Conference on B and Z","article-title":"Automatic translation from UML specifications to B","author":"Ledang","year":"2002"},{"key":"10.3166\/ejc.12.115-130_bib0115","series-title":"proceedings of the ASI annual Conference of the ICIMS-NOE","article-title":"From discrete event behavioural modelling to intelligent actuation and measurement modelling","author":"Lhoste","year":"1996"},{"issue":"11","key":"10.3166\/ejc.12.115-130_bib0120","first-page":"1","article-title":"The extension of principles of cybernetics towards engineering and manufacturing","volume":"23","author":"Lhote","year":"1999","journal-title":"IFAC Annu. Rev. Control"},{"key":"10.3166\/ejc.12.115-130_bib0125","doi-asserted-by":"crossref","first-page":"501","DOI":"10.1016\/S0967-0661(98)00047-1","article-title":"Physical system modelling with Modelica","volume":"6","author":"Mattsson","year":"1998","journal-title":"Control Eng Practice"},{"key":"10.3166\/ejc.12.115-130_bib0130","isbn-type":"print","author":"Mellor","year":"2004","ISBN":"http:\/\/id.crossref.org\/isbn\/0201788918"},{"key":"10.3166\/ejc.12.115-130_bib0135","first-page":"45","article-title":"Engineering-related formal method for the development of safe industrial automation systems","volume":"1","author":"Moik","year":"2003","journal-title":"Autom Technol Practice Int J"},{"key":"10.3166\/ejc.12.115-130_bib0140","series-title":"7th IFAC Symposium on Cost Oriented Automation, COA\u20192004, Gatineau","article-title":"Proof-oriented fault-tolerant systems engineering: rationales, experiments and open issues","author":"Morel","year":"2004"},{"issue":"2","key":"10.3166\/ejc.12.115-130_bib0145","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1504\/IJIEM.2005.007638","article-title":"Metamodelling of production systems process models using UML stereotypes","volume":"3","author":"Panetto","year":"2005","journal-title":"Int J Internet Enter Manage"},{"key":"10.3166\/ejc.12.115-130_bib0150","series-title":"IFAC\/INCOM2004 symposium","article-title":"Controller dependability analysis by probabilistic model checking","author":"Parker","year":"2004"},{"key":"10.3166\/ejc.12.115-130_bib0155","unstructured":"Paynter M. Analysis and design of engineering systems, M.I.T. Press, Cambridge, ISBN 0-262r-r16004-8."},{"key":"10.3166\/ejc.12.115-130_bib0160","doi-asserted-by":"crossref","unstructured":"Petin JF, Iung B, Morel G. Distributed intelligent actuation and measurement system within an integrated shop-floor organisation, Comput Industry J 37: 197-211.","DOI":"10.1016\/S0166-3615(98)00099-2"},{"key":"10.3166\/ejc.12.115-130_bib0165","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1007\/BFb0053362","article-title":"Process control engineering: contribution to a formal structuring framework with the B method","volume":"1393","author":"P\u00e9tin","year":"1998","journal-title":"Lectures notes in Computer Science"},{"key":"10.3166\/ejc.12.115-130_bib0170","first-page":"49","article-title":"Ease of use in engineering \u2013 availability and safety during runtime","volume":"1","author":"Polzer","year":"2004","journal-title":"Autom Technol Practice Int J"},{"key":"10.3166\/ejc.12.115-130_bib0175","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","article-title":"Supervisory control of a class of discrete event processes","author":"Ramadge","year":"1987","journal-title":"SIAM J Control Optim"},{"key":"10.3166\/ejc.12.115-130_bib0180","series-title":"6th IFAC \/WODES","first-page":"303","article-title":"An algebraic approach for PLC programs verification","author":"Roussel","year":"2002"},{"key":"10.3166\/ejc.12.115-130_bib0185","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/BFb0057795","article-title":"Using UML for modelling complex real-time systems","volume":"1474","author":"Selic","year":"1998","journal-title":"Lectures Notes in Computer Science"},{"key":"10.3166\/ejc.12.115-130_bib0190","first-page":"4","article-title":"Systems functions implementation and behavioural modelling: system theoretic approach","author":"Shell","year":"2001","journal-title":"Int J Systems Eng"},{"key":"10.3166\/ejc.12.115-130_bib0195","author":"Wright","year":"1988"}],"container-title":["European Journal of Control"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0947358006710184?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0947358006710184?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,26]],"date-time":"2019-04-26T19:11:07Z","timestamp":1556305867000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0947358006710184"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,1]]}},"alternative-id":["S0947358006710184"],"URL":"https:\/\/doi.org\/10.3166\/ejc.12.115-130","relation":{},"ISSN":["0947-3580"],"issn-type":[{"value":"0947-3580","type":"print"}],"subject":[],"published":{"date-parts":[[2006,1]]}}}