{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,13]],"date-time":"2025-02-13T05:21:18Z","timestamp":1739424078956,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642044243"},{"type":"electronic","value":"9783642044250"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04425-0_34","type":"book-chapter","created":{"date-parts":[[2009,9,30]],"date-time":"2009-09-30T09:52:04Z","timestamp":1254304324000},"page":"438-452","source":"Crossref","is-referenced-by-count":24,"title":["Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation"],"prefix":"10.1007","author":[{"given":"Philippe","family":"Dhaussy","sequence":"first","affiliation":[]},{"given":"Pierre-Yves","family":"Pillain","sequence":"additional","affiliation":[]},{"given":"Stephen","family":"Creff","sequence":"additional","affiliation":[]},{"given":"Amine","family":"Raji","sequence":"additional","affiliation":[]},{"given":"Yves","family":"Le Traon","sequence":"additional","affiliation":[]},{"given":"Benoit","family":"Baudry","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"34_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"2004","unstructured":"Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical computer Science\u00a0126(2), 183\u2013235 (2004)","journal-title":"Theoretical computer Science"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/3-540-45657-0_26","volume-title":"Computer Aided Verification","author":"M. Bozga","year":"2002","unstructured":"Bozga, M., Graf, S., Mounier, L.: IF2: A validation environment for component-based real-time systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 343. Springer, Heidelberg (2002)"},{"key":"34_CR3","unstructured":"Clarke, T., Evans, A., Sammut, P., Willians, J.: Applied Meamodeling: A foundation for Language Driven Development. Technical report, version 0.1, Xactium (2004)"},{"key":"34_CR4","unstructured":"ITU-T. Recommendations Z-100. Specification and Description Language (SDL) (1994)"},{"key":"34_CR5","first-page":"411","volume-title":"Proc. of the 21st Int. Conf. on Software Engineering","author":"M.B. Dwyer","year":"1999","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proc. of the 21st Int. Conf. on Software Engineering, pp. 411\u2013420. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Lagnier, F., Raymond, P.: Synchronous observers and the verification of reactive systems. In: 3rd int. Conf. on Algebraic Methodology and Software Technology, AMAST 1993 (1993)","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"Haugen, O., Husa, K.E., Runde, R.K., Stolen, K.: Stairs: Towards formal design with sequence diagrams. Journal of Software and System Modeling (2005)","DOI":"10.1007\/s10270-005-0087-0"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"J.-C. Fernandez","year":"1996","unstructured":"Fernandez, J.-C., et al.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/3-540-48234-2_7","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"W. Janssen","year":"1999","unstructured":"Janssen, W., Mateescu, R., Mauw, S., Fennema, P., Stappen, P.: Model Checking for Managers. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 92\u2013107. Springer, Heidelberg (1999)"},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"Konrad, S., Cheng, B.: Real-Time Specification Patterns. In: Proc. of the 27th Int. Conf. on Software Engineering (ICSE 2005), St Louis, MO, USA (2005)","DOI":"10.1145\/1062455.1062526"},{"key":"34_CR11","unstructured":"Roger, J.C.: Exploitation de contextes et d\u2019observateurs pour la v\u00e9rification formelle de mod\u00e8les, Phd report, Univ. of Rennes I (2006)"},{"key":"34_CR12","first-page":"11","volume-title":"Proc. of the 24th Int. Conf. on Software Engineering","author":"R. Smith","year":"2002","unstructured":"Smith, R., Avrunin, G.S., Clarke, L., Osterweil, L.: Propel: An Approach Supporting Property Elucidation. In: Proc. of the 24th Int. Conf. on Software Engineering, pp. 11\u201321. ACM Press, New York (2002)"},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"Whittle J.: Specifying precise use cases with use case charts. In MoDELS 2006, Satellite Events, pp. 290\u2013301 (2005)","DOI":"10.1007\/11663430_30"},{"key":"34_CR14","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Vernadat, F.: Time Petri nets analysis with TINA. In: 3rd Int. Conf. on the Quantitative Evaluation of Systems (QEST 2006), Riverside, USA, pp. 123\u2013124 (2006)","DOI":"10.1109\/QEST.2006.56"},{"key":"34_CR15","unstructured":"Berthomieu, B., Bodeveix, J., Filali, M., Garavel, H., Lang, F., Peres, F., Saad, R., Stoecker, J., Vernadat, F.: The Syntax and Semantics of FIACRE, Version 1.0 alpha. Technical report projet ANR05RNTL03101 OpenEmbeDD (2007)"},{"key":"34_CR16","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"2","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst.\u00a02, 244\u2013263 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"34_CR17","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/s10270-007-0076-6","volume":"8","author":"J. Hassine","year":"2009","unstructured":"Hassine, J., Rilling, J., Dssouli, R.: Use Case Maps as a property specification language. Software System Model\u00a08, 205\u2013220 (2009)","journal-title":"Software System Model"},{"key":"34_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The temporal logic of reactive and concurrent systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems. Springer, New York (1992)"},{"key":"34_CR19","doi-asserted-by":"crossref","unstructured":"Feiler, P., Gluch, D.P., Hudak, J.J.: The Architecture Analysis and Design Language (AADL): An introduction.Technical report, Society of Automotive Engineers, SAE (2006)","DOI":"10.21236\/ADA455842"},{"key":"34_CR20","doi-asserted-by":"crossref","unstructured":"Dhaussy, P., Boniol, F.: Mise en \u0153uvre de composants MDA pour la validation formelle de mod\u00e8les de syst\u00e8mes d\u2019information embarqu\u00e9s, pp. 133\u2013157. RSTI (2007)","DOI":"10.3166\/isi.12.5.133-157"},{"key":"34_CR21","doi-asserted-by":"crossref","unstructured":"Dhaussy P., Auvray J., De Belloy S., Boniol F., Landel E.: Using context descriptions and property definition patterns for software formal verification, Workshop Modevva 2008 (hosted by ICST 2008), Lillehammer, Norway (2008)","DOI":"10.1109\/ICSTW.2008.52"},{"key":"34_CR22","unstructured":"Dhaussy, P., Creff, S., Pillain, P.Y., Leilde, V.: CDL language specification (Context Description Language). Technical report version N\u00b0 DTN\/2009\/8, ENSIETA (2009)"}],"container-title":["Lecture Notes in Computer Science","Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04425-0_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T12:48:46Z","timestamp":1739364526000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04425-0_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642044243","9783642044250"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04425-0_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}