{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T12:05:46Z","timestamp":1648814746324},"reference-count":44,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1991,1,1]],"date-time":"1991-01-01T00:00:00Z","timestamp":662688000000},"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":["Information Systems"],"published-print":{"date-parts":[[1991,1]]},"DOI":"10.1016\/0306-4379(91)90001-p","type":"journal-article","created":{"date-parts":[[2003,8,8]],"date-time":"2003-08-08T01:31:39Z","timestamp":1060306299000},"page":"245-272","source":"Crossref","is-referenced-by-count":2,"title":["Formal techniques for systems specification and verification"],"prefix":"10.1016","volume":"16","author":[{"given":"Jos\u00e9","family":"Carmo","sequence":"first","affiliation":[]},{"given":"Am\u00edlcar","family":"Sernadas","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0306-4379(91)90001-P_BIB1","article-title":"Software behavior specification with triggering logic","author":"Sernadas","year":"1982"},{"key":"10.1016\/0306-4379(91)90001-P_BIB2","series-title":"Infolog PRO5, IFIP WG 8.1 Meeting","article-title":"Infolog: an integrated model of data and processes","author":"Sernadas","year":"1983"},{"key":"10.1016\/0306-4379(91)90001-P_BIB3","series-title":"Knowledge Representation for DDS","article-title":"Capturing knowledge about the organization dynamics","author":"Sernadas","year":"1985"},{"key":"10.1016\/0306-4379(91)90001-P_BIB4","first-page":"91","article-title":"Conceptual modelling for knowledge-based DSS development","author":"Sernadas","year":"1987"},{"key":"10.1016\/0306-4379(91)90001-P_BIB5","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/0306-4379(80)90009-5","article-title":"Temporal aspects of logical procedure definition","volume":"5","author":"Sernadas","year":"1980","journal-title":"Information Systems"},{"key":"10.1016\/0306-4379(91)90001-P_BIB6","series-title":"Proc. 8th VLDB Conf.","first-page":"280","article-title":"A temporal framework for information systems specification","author":"Castilho","year":"1982"},{"key":"10.1016\/0306-4379(91)90001-P_BIB7","series-title":"Proc 9th VLDB Conf.","first-page":"331","article-title":"A modal system of algebras for database specification and query\/update language support","author":"Golshani","year":"1983"},{"key":"10.1016\/0306-4379(91)90001-P_BIB8","article-title":"A temporal framework for information systems specification and verification","author":"Kung","year":"1984"},{"key":"10.1016\/0306-4379(91)90001-P_BIB9","series-title":"Theoretical and Formal Aspects of Information Systems 1985","first-page":"145","article-title":"Specifying admissibility of dynamic database behavior using temporal logic","author":"Lipeck","year":"1985"},{"key":"10.1016\/0306-4379(91)90001-P_BIB10","series-title":"Proc. 18th Annual ACM Symp. on Foundations of Computer Science, IEEE","first-page":"45","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/0306-4379(91)90001-P_BIB11","series-title":"The Correctness Problem in Computer Science","first-page":"215","article-title":"Verification of concurrent programs: the temporal framework","author":"Manna","year":"1981"},{"key":"10.1016\/0306-4379(91)90001-P_BIB12","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","article-title":"Proving liveness properties of concurrent programs","volume":"4","author":"Owicki","year":"1982","journal-title":"ACM TOPLAS"},{"key":"10.1016\/0306-4379(91)90001-P_BIB13","series-title":"Formal Technics for Data Base Design","author":"Furtado","year":"1986"},{"key":"10.1016\/0306-4379(91)90001-P_BIB14","series-title":"Temporal Aspects in Information Systems","first-page":"31","article-title":"A temporal logic framework for a layered approach to systems specification and verification","author":"Carmo","year":"1988"},{"key":"10.1016\/0306-4379(91)90001-P_BIB15","series-title":"Theoretical and Formal Aspects of Information Systems 1985","first-page":"191","article-title":"A tableaux approach for consistency checking","author":"Kung","year":"1985"},{"key":"10.1016\/0306-4379(91)90001-P_BIB16","series-title":"A Mathematical Introduction to Logic","author":"Enderton","year":"1972"},{"key":"10.1016\/0306-4379(91)90001-P_BIB17","series-title":"Architecture and Models in Database Management","article-title":"The temporal dimension in information processing","author":"Bubenko","year":"1977"},{"key":"10.1016\/0306-4379(91)90001-P_BIB18","series-title":"Proc. 5th VLDB Conf.","article-title":"Tools for information systems dynamics management","author":"Rolland","year":"1979"},{"key":"10.1016\/0306-4379(91)90001-P_BIB19","series-title":"Past, Present and Future","author":"Prior","year":"1967"},{"key":"10.1016\/0306-4379(91)90001-P_BIB20","series-title":"Temporal Logic","author":"Rescher","year":"1971"},{"key":"10.1016\/0306-4379(91)90001-P_BIB21","series-title":"Proc. Workshop on Logic of Programs","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"Clarke","year":"1981"},{"key":"10.1016\/0306-4379(91)90001-P_BIB22","article-title":"Proving precedence properties: the temporal way","author":"Manna","year":"1984"},{"key":"10.1016\/0306-4379(91)90001-P_BIB23","series-title":"Theoretical and Formal Aspects of Information Systems 1985","first-page":"159","article-title":"The Infolog branching logic of events","author":"Carmo","year":"1985"},{"key":"10.1016\/0306-4379(91)90001-P_BIB24","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/0306-4379(86)90023-2","article-title":"The Infolog linear tense propositional logic of events and transactions","volume":"11","author":"Fiadeiro","year":"1986","journal-title":"Information Systems"},{"key":"10.1016\/0306-4379(91)90001-P_BIB25","series-title":"Proc. 7th Annual ACM Symp. on Principles of Programming Languages, ACM","first-page":"174","article-title":"\u201cSometime\u201d is sometimes \u201cnot never\u201d on the temporal logic of programs","author":"Lamport","year":"1980"},{"key":"10.1016\/0306-4379(91)90001-P_BIB26","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"Sometimes and \u201cnot never\u201d revisited: on branching versus linear time temporal logic","volume":"33","author":"Emerson","year":"1986","journal-title":"J. ACM"},{"key":"10.1016\/0306-4379(91)90001-P_BIB27","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/BF01888216","article-title":"Branching versus linear logics yet again","volume":"2","author":"Carmo","year":"1990","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/0306-4379(91)90001-P_BIB28","article-title":"L\u00f3gicas temporais para a especifica\u00e7\u00e3o e verifica\u00e7\u00e3o de sistemas de informa\u00e7\u00e3o","author":"Carmo","year":"1988"},{"key":"10.1016\/0306-4379(91)90001-P_BIB29","doi-asserted-by":"crossref","first-page":"625","DOI":"10.1007\/BF00291052","article-title":"Specification and verification of database dynamics","volume":"25","author":"Fiadeiro","year":"1988","journal-title":"Acta Informatica"},{"key":"10.1016\/0306-4379(91)90001-P_BIB30","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","article-title":"Petri Nets, event structures, and domains","volume":"13","author":"Nielsen","year":"1980","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0306-4379(91)90001-P_BIB31","series-title":"Proc. ICALP'82, LNCS 140","first-page":"561","article-title":"Event structure semantics for CCS and related languages","author":"Winskell","year":"1982"},{"key":"10.1016\/0306-4379(91)90001-P_BIB32","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF01379149","article-title":"Modelling concurrency with partial orders","volume":"15","author":"Pratt","year":"1987","journal-title":"Int. J. Parallel Program"},{"key":"10.1016\/0306-4379(91)90001-P_BIB33","first-page":"181","article-title":"Concurrency is more fundamental than interleaving","volume":"35","author":"Reisig","year":"1988","journal-title":"EATCS Bull."},{"key":"10.1016\/0306-4379(91)90001-P_BIB34","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"10.1016\/0306-4379(91)90001-P_BIB35","series-title":"Proc. 7th Annual ACM Symp. on Principles of Programming Languages, ACM","first-page":"163","article-title":"On the temporal analysis of fairness","author":"Gabbay","year":"1980"},{"key":"10.1016\/0306-4379(91)90001-P_BIB36","series-title":"Theoretical and Formal Aspects of Information Systems 1985","first-page":"175","article-title":"Towards simpler and yet complete formal specifications","author":"Veloso","year":"1985"},{"key":"10.1016\/0306-4379(91)90001-P_BIB37","series-title":"Temporal Aspects in Information Systems","first-page":"77","article-title":"Behavioral aspects of intelligent knowledge based information systems","author":"Fiadeiro","year":"1988"},{"key":"10.1016\/0306-4379(91)90001-P_BIB38","series-title":"An Introduction to Modal Logic","author":"Hughes","year":"1968"},{"key":"10.1016\/0306-4379(91)90001-P_BIB39","series-title":"Tense Logic","author":"McArthur","year":"1976"},{"key":"10.1016\/0306-4379(91)90001-P_BIB40","article-title":"On tense logic and the theory of linear order","author":"Kamp","year":"1968"},{"key":"10.1016\/0306-4379(91)90001-P_BIB41_1","series-title":"Proc. 14th Annual ACM Symp on Theory of Computing, ACM","first-page":"169","article-title":"Decision procedures and expressivness in the temporal logic of branching time","author":"Emerson","year":"1982"},{"key":"10.1016\/0306-4379(91)90001-P_BIB41_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"Emerson","year":"1985","journal-title":"J. Comput. Syst. Sci."},{"key":"10.1016\/0306-4379(91)90001-P_BIB42","series-title":"Proc. of the 13th VLDB Conf.","first-page":"107","article-title":"Object-oriented specification of databases: an algebraic approach","author":"Sernadas","year":"1987"},{"key":"10.1016\/0306-4379(91)90001-P_BIB43","series-title":"Advances in Object-oriented Database Systems","first-page":"144","article-title":"Abstract object types for databases","author":"Ehrich","year":"1988"}],"container-title":["Information Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030643799190001P?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030643799190001P?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T04:55:10Z","timestamp":1552625710000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030643799190001P"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,1]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1991,1]]}},"alternative-id":["030643799190001P"],"URL":"https:\/\/doi.org\/10.1016\/0306-4379(91)90001-p","relation":{},"ISSN":["0306-4379"],"issn-type":[{"value":"0306-4379","type":"print"}],"subject":[],"published":{"date-parts":[[1991,1]]}}}