{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:33:22Z","timestamp":1725489202730},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417910"},{"type":"electronic","value":"9783540452515"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45251-6_34","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T05:53:28Z","timestamp":1186898008000},"page":"590-610","source":"Crossref","is-referenced-by-count":1,"title":["A Modular Approach to the Specification and Validation of an Electrical Flight Control System"],"prefix":"10.1007","author":[{"given":"M.","family":"Doche","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"I.","family":"Vernier-Mounier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F.","family":"Kordon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,3,16]]},"reference":[{"key":"34_CR1","unstructured":"Action FORMA. Ma\u00eetrise de syst\u00e8mes complexes r\u00e9actifs et s\u00fbrs, Journ\u00e9e au MENRT: Bilan de la 1ereann\u00e9e, Paris, January 1998. http:\/\/www.imag.fr\/FORMA\/ ."},{"key":"34_CR2","doi-asserted-by":"crossref","unstructured":"R; Alur, T.A. henzinger, F.Y.C. Mang, S. Qadeer, S.K. Rajamani, and S. Tasiran. Mocha: Modularity in model checking. In proceedings on the 10th International Conference on Computer-Aided Verification, pages 521\u2013525. Springer Verlag, 1998.","DOI":"10.1007\/BFb0028774"},{"key":"34_CR3","doi-asserted-by":"crossref","unstructured":"H.R. Andersen, J. Staunstrup, and N. Maretti. A comparison of modular verification techniques. In Proceedings of FASE\u201997. Springer Verlag, 1997.","DOI":"10.1007\/BFb0030625"},{"key":"34_CR4","doi-asserted-by":"crossref","unstructured":"R.J. Anderson, P. Beame, S. Burns, W. Chan, F. Modugno, D. Notkin, and J.D. Reese. Model checking large software specifications. In Proceedings of the 4th ACM SIGOFT Symposium on the Foundations of Software engineering, pages 156\u2013166, 1996.","DOI":"10.1145\/239098.239127"},{"key":"34_CR5","unstructured":"S. Barbey, D. Buchs, M-C. Gaudel, B. Marre, C. P\u00e9raire, P. Th\u00e9evenod-Fosse, and H. Waeselynck. From requirements to tests via object-oriented design. Technical Report 20072, DeVa ESPRIT Long Term Research Project, 1998. http:\/\/www.laas.research.ec.org\/deva\/papers\/4c.pdf ."},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"G. Bernot, M-C. Gaudel, and B. Marre. Software testing based on formal specifications: a theory and a tool. Software Engineering Journal, 6, November 1991.","DOI":"10.1049\/sej.1991.0040"},{"key":"34_CR7","first-page":"616","volume":"23","author":"D. Bri\u00e8re","year":"1993","unstructured":"D. Bri\u00e8re and P. Traverse. Airbus a320\/a330\/a340 electric flight controls: a family of fault-tolerant systems. FTCS, 23:616\u2013623, 1993.","journal-title":"FTCS"},{"key":"34_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1007\/3-540-48683-6_6","volume-title":"CAV\u201999","author":"E. Brinksma","year":"1999","unstructured":"E. Brinksma. Formal methods for conformance testing: Theory can be practical. In CAV\u201999, number 1633 in LNCS, pages 44\u201346. Springer Verlag, July 1999."},{"key":"34_CR9","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"4","author":"J.R. Burch","year":"1994","unstructured":"J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. DILL. Symbolic model checking for sequential circuit verification. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 13, 4:401\u2013424, 1994.","journal-title":"IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems 13"},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"W. Chan, R.J. Anderson, P. Beame, and D. Notkin. Improving A efficiency of Symbolic Model Checking for State-Based System Requirements. In proceedings of the 1998 International Symposium on Software Testing and Analysis, 1998.","DOI":"10.1145\/271771.271798"},{"key":"34_CR11","unstructured":"E. Ciapessoni, E. Corsetti, M. Migliorati, and E. Ratto. Specifying industrial real-time systems in a logical framework. In ICLP 94-Post Conference Workshop on Logic Programming in Software Engineering, 1994."},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and J.M. Wing. Formal Methods: State of the Art and Future Directions. Technical report, Carnegie Mellon University, 1996.","DOI":"10.1145\/242223.242257"},{"key":"34_CR13","volume-title":"LIP6","author":"A. Diagne","year":"1997","unstructured":"A. Diagne. Une Approche Multi-Formalismes de Sp\u00e9cification de Syst\u00e8mes R\u00e9partis: Transformations de Composants Modulaires en R\u00e9seaux de Petri. Th\u00e8se, LIP6, Universit\u00e9 Paris 6, 4, Place Jussieu, 75252 Paris Cedex 05, May 1997."},{"key":"34_CR14","unstructured":"A. Diagne and F. Kordon. A multi-formalisms prototyping approach from conceptual description to implementation of distributed systems. In Proceedings of the 7th IEEE International Workshop on Rapid System Prototyping (RSP\u201996), Porto Caras, Thessaloniki Greece, June 1996."},{"key":"34_CR15","unstructured":"M. Doche. Techniques formelles pour l\u2019\u00e9valuation de syst\u00e8mes complexes. Test et modularit\u00e9. PhD thesis, ENSAE, ONERA-CERT\/DTIM, D\u00e9cembre 1999."},{"key":"34_CR16","unstructured":"M. Doche, J. Cazin, D. Le Berre, P. Michel, C. Seguin, and V. Wiels. Module templates for the specification of fault-tolerant systems. In DASIA\u201998, May 1998."},{"key":"34_CR17","unstructured":"M. Doche, C. Seguin, and V. Wiels. A modular approach to specify and test an electrical flight control system. In FMICS-4, Fourth International Workshop on formal Methods for Industrial Critical Systems, July 1999. Available at http:\/\/www.cert.fr\/francais\/deri\/wiels\/Publi\/fmics99.ps ."},{"key":"34_CR18","series-title":"Lect Notes Comput Sci","volume-title":"AMAST00, Algebraic Methodology And Software Technology","author":"M. Doche","year":"2000","unstructured":"M. Doche and V. Wiels. Extended institutions for testing. In AMAST00, Algebraic Methodology And Software Technology, LNCS, Iowa City, May 2000. Springer Verlag. Available at http:\/\/www.cert.fr\/francais\/deri\/wiels\/Publi\/amast00.ps ."},{"key":"34_CR19","unstructured":"ECMA. A Reference Model for Frameworks of Software Engineerings Environments. Technical Report TR\/55 (version 3), NIST Report, 1993."},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2: Modules specifications and constraints, volume 21 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1990.","DOI":"10.1007\/978-3-642-61284-8_8"},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"M-C. Gaudel. Testing can be formal, too. In TAPSOFT\u201995, pages 82\u201396. Springer Verlag, 1995.","DOI":"10.1007\/3-540-59293-8_188"},{"issue":"4","key":"34_CR22","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1145\/133233.129397","volume":"14","author":"C. Ghezzi","year":"1992","unstructured":"C. Ghezzi, D. Mandrioli, and A. Morzenti. A model parametric real-time logic. ACM Transactions on programming languages and systems, 14(4):521\u2013573, October 1992.","journal-title":"ACM Transactions on programming languages and systems"},{"issue":"1","key":"34_CR23","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J. A. Goguen","year":"1992","unstructured":"J. A. Goguen and R. Burstall. Institutions: Abstract model theory for specification and programming. Journal of the ACM, 39(1):95\u2013146, January 1992.","journal-title":"Journal of the ACM"},{"key":"34_CR24","doi-asserted-by":"crossref","unstructured":"K. Jensen. Coloured Petri Nets, Basic Concepts, Analysis Methods and Practical Use, Volumes 1, 2 and 3. Springer-Verlag, 1992.","DOI":"10.1007\/978-3-662-06289-0_1"},{"key":"34_CR25","unstructured":"MARS-Team. MARS Home page. http:\/\/www.lip6.fr\/mars ."},{"key":"34_CR26","doi-asserted-by":"crossref","unstructured":"P. Michel and V. Wiels. A Framework for Modular Formal Specification and Verification. In LNCS 1313, Proceedings of FME\u201997, September 1997.","DOI":"10.1007\/3-540-63533-5_28"},{"key":"34_CR27","doi-asserted-by":"crossref","unstructured":"A. Morzenti, P. San Pietro, and S. Morasca. A tool for automated system analysis based on modular specifications. In ASE98, pages 2\u201311. IEEE Computer Society, 1998.","DOI":"10.1109\/ASE.1998.732560"},{"key":"34_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/3-540-60973-3_100","volume-title":"Automatic verification of a hydroelectric power plant","author":"R. Pugliese","year":"1996","unstructured":"R. Pugliese and E. Tronci. Automatic verification of a hydroelectric power plant. In LNCS 1051, FME\u201996: Industrial Benefit and Advances in Formal Methods, 3rd International Symposium of Formal Methods Europe, pages 425\u2013444, 1996."},{"key":"34_CR29","doi-asserted-by":"crossref","unstructured":"T. Sreemani and J.M. Atlee. Feasibility of model checking software requirements: A case study. In COMPASS\u2019]96, Proceedings of the 11th Annual Conference on Computer Assurance, pages 77\u201388, 1996.","DOI":"10.1109\/CMPASS.1996.507877"},{"key":"34_CR30","series-title":"Technical Report","isbn-type":"print","volume-title":"PROD Reference Manual","author":"K. Varpaaniemi","year":"1995","unstructured":"K. Varpaaniemi, J. Halme, K. Hiekkanen, and T. Pyssysalo. PROD Reference Manual. Technical Report ISBN 951-22-2707-X, University of technology, Departement of Computer Science, Digital Systems Laboratory, 1995.","ISBN":"http:\/\/id.crossref.org\/isbn\/951222707X"},{"key":"34_CR31","unstructured":"V. Wiels. Modularit\u00e9 pour la conception et la validation formelles de syst\u00e8mes. PhD thesis, ENSAE-ONERA\/CERT, October 1997."}],"container-title":["Lecture Notes in Computer Science","FME 2001: Formal Methods for Increasing Software Productivity"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45251-6_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:49:08Z","timestamp":1556754548000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45251-6_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417910","9783540452515"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-45251-6_34","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}