{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T11:27:27Z","timestamp":1746012447025},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,6,29]],"date-time":"2006-06-29T00:00:00Z","timestamp":1151539200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2007,2,7]]},"DOI":"10.1007\/s10009-006-0007-9","type":"journal-article","created":{"date-parts":[[2006,6,28]],"date-time":"2006-06-28T11:38:24Z","timestamp":1151494704000},"page":"77-88","source":"Crossref","is-referenced-by-count":4,"title":["CTL-property Transformations along an Incremental Design Process"],"prefix":"10.1007","volume":"9","author":[{"given":"C\u00e9cile","family":"Braunstein","sequence":"first","affiliation":[]},{"given":"Emmanuelle","family":"Encrenaz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,29]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, TA., Mang, FYC., Qadeer, S., Rajamani, SK., Tasiran, S.:MOCHA: modularity in model checking. In CAV\u201998: Proceedings of the 10th International Conference on Computer Aided Verification, vol. 1427. Lecture Notes in Computer Science, pp. 521\u2013525, Springer, Berlin Heidelberg New York (1998)","DOI":"10.1007\/BFb0028774"},{"issue":"2","key":"7_CR2","first-page":"142","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"Burch J.R., Clarke E.M., McMillan K.L., Dill D.L., Hwang L.J. (1992). Symbolic model checking: 1020 states and beyond. In. Comput. 98(2):142\u2013170 Special issue for best papers from LICS\u201990","journal-title":"In. Comput."},{"key":"7_CR3","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/978-1-4471-0287-8_5","volume-title":"Language Constructs for Designing Features","author":"D. Cansell","year":"2001","unstructured":"Cansell D., M\u00e9ry D. (2001). Abstraction and refinement of features. In: Gilmore S., Ryan M. (eds) Language Constructs for Designing Features. Springer, Berlin Heidelberg New York, pp. 65\u201384"},{"key":"7_CR4","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/978-1-4471-0287-8_6","volume-title":"Language Constructs for Describing Features","author":"F. Cassez","year":"2001","unstructured":"Cassez F., Ryan M., Schobbens P-Y. (2001). Proving feature non-interaction with alternating-time temporal logic. In: Gilmore S., Ryan M. (eds) Language Constructs for Describing Features. Springer, Berlin Heidelberg New York, pp. 85\u2013104"},{"key":"7_CR5","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke E.M., Grumberg O., Peled D.A. (1999). Model Checking. The MIT Press, Cambridge"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. In: International Conference on Concurrency Theory. vol. 527. Lecture Notes in Computer Science, pp. 250\u2013263. Springer Berlin Heidelberg New York (1991)","DOI":"10.1007\/3-540-54430-5_93"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: You assume, we guarantee: methodology and case studies. In: Computer Aided Verification, vol. 1427. Lecture Notes in Computer Science, pp. 440\u2013451, Springer, Berlin Heidelberg New York (1998)","DOI":"10.1007\/BFb0028765"},{"key":"7_CR8","volume-title":"The B Language and Method, A guide to Practical Formal Development","author":"K. Lano","year":"1996","unstructured":"Lano K. (1996). The B Language and Method, A guide to Practical Formal Development. Springer, Secaucus"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Third Annual Symposium on Logic in Computer Science, pp. 203\u2013210, Edinburgh, Scotland, UK, IEEE Computer Society (1988)","DOI":"10.1109\/LICS.1988.5119"},{"issue":"1","key":"7_CR10","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C. Loiseaux","year":"1995","unstructured":"Loiseaux C., Graf S., Sifakis J., Bouajjani A., Bensalem S. (1995). Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6(1):11\u201344","journal-title":"Formal Methods in System Design"},{"key":"7_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan K.L. (1993). Symbolic model checking. Kluwer, Dordrecht"},{"key":"7_CR12","unstructured":"On-Chip Bus Development Working Group. Virtual Component Interface Standard (VCI). VSI Alliance (2000)"},{"key":"7_CR13","unstructured":"Open Microprocessors System Initiatives. OMI324: PI-Bus Standard Specification. Siemens, Munich, Germany (1994)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Pasareanu, C.S., Dwyer, M.B., Huth, M.: Assume-guarantee model checking of software: a comparative case study. In: Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, pp. 168\u2013183 Springer, London, UK (1999)","DOI":"10.1007\/3-540-48234-2_14"},{"issue":"1","key":"7_CR15","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/S0167-6423(00)00018-6","volume":"41","author":"M. Plath","year":"2001","unstructured":"Plath M., Ryan M. (2001). Feature integration using a feature construct. Sci. Comput. Program. 41(1):53\u201384","journal-title":"Sci. Comput. Program."},{"key":"7_CR16","unstructured":"STERIA Technologie de l\u2019information. Atelier B, Manuel Utilisateur. Aix-en-Provence, France (1998)"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"The VIS group. VIS : A System for Verification and Synthesis. In: International Conference on Computer-Aided Verification, vol. 1102. Lecture Notes in Computer Science, pp. 428\u2013432. Springer, Berlin Heidelberg New York (1996)","DOI":"10.1007\/3-540-61474-5_95"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0007-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-006-0007-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0007-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:22Z","timestamp":1559114722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-006-0007-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,6,29]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,2,7]]}},"alternative-id":["7"],"URL":"https:\/\/doi.org\/10.1007\/s10009-006-0007-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,6,29]]}}}