{"_id":"qmRHSvaNqARpkTRQg","bibbaseid":"felix-haeusler-soares-validatinghypermediadocumentsatimedautomataapproach-2001","downloads":0,"creationDate":"2017-07-16T16:26:30.388Z","title":"Validating hypermedia documents: a timed automata approach","author_short":["Felix, M.","Haeusler, E. H.","Soares, L. F. G."],"year":2001,"bibtype":"report","biburl":"http://www.telemidia.puc-rio.br/files/biblio/all.bib","bibdata":{"bibtype":"report","type":"report","location":"Rio de Janeiro, Brasil","title":"Validating hypermedia documents: a timed automata approach","abstract":"This paper presents a formal approach to validating hypermedia documents, a case of real-time and reactive computing application, aiming to extend these ideas to the contex of architectural design. The main aspect of hypermedia validation concerns to the so-called temporal consistency analysis problem: a document is consistent if it is possible present it in a way that all the event synchronization constraints can be fulfilled. The validation technique consists in providing formal semantics to hypermedia documents via network of timed-automata, in a compositional way. Therefore, obtained a behavioral model of the document, we can pass to the model-checking phase. The consistency analysis consists on to formulate an adequate set of temporal logic formulas that will be checked against to the automata model. The specifications of the hypermedia documents that we are written using the modeling concepts of NCM (Nested Context Model), a conceptual model to hypermedia documents, and we choose UPPAAL as the model-checking tool to implement the our hypermedia validation model. This work as well constitutes a preliminary investigation, via a case study, about how we can integrate formal validation, using model-checking techniques, with software architecture design.","author":[{"propositions":[],"lastnames":["Felix"],"firstnames":["M.F."],"suffixes":[]},{"propositions":[],"lastnames":["Haeusler"],"firstnames":["Edward","Hermann"],"suffixes":[]},{"propositions":[],"lastnames":["Soares"],"firstnames":["Luiz","Fernando","Gomes"],"suffixes":[]}],"year":"2001","bibtex":"@report{felix_validating_2001,\n\tlocation = {Rio de Janeiro, Brasil},\n\ttitle = {Validating hypermedia documents: a timed automata approach},\n\tabstract = {This paper presents a formal approach to validating hypermedia documents, a case of real-time and reactive computing application, aiming to extend these ideas to the contex of architectural design. The main aspect of hypermedia validation concerns to the so-called temporal consistency analysis problem: a document is consistent if it is possible present it in a way that all the event synchronization constraints can be fulfilled. The validation technique consists in providing formal semantics to hypermedia documents via network of timed-automata, in a compositional way. Therefore, obtained a behavioral model of the document, we can pass to the model-checking phase. The consistency analysis consists on to formulate an adequate set of temporal logic formulas that will be checked against to the automata model. The specifications of the hypermedia documents that we are written using the modeling concepts of {NCM} (Nested Context Model), a conceptual model to hypermedia documents, and we choose {UPPAAL} as the model-checking tool to implement the our hypermedia validation model. This work as well constitutes a preliminary investigation, via a case study, about how we can integrate formal validation, using model-checking techniques, with software architecture design.},\n\tauthor = {Felix, M.F. and Haeusler, Edward Hermann and Soares, Luiz Fernando Gomes},\n\tyear = {2001},\n}\n\n","author_short":["Felix, M.","Haeusler, E. H.","Soares, L. F. G."],"key":"felix_validating_2001","id":"felix_validating_2001","bibbaseid":"felix-haeusler-soares-validatinghypermediadocumentsatimedautomataapproach-2001","role":"author","urls":{},"metadata":{"authorlinks":{}},"downloads":0,"html":""},"search_terms":["validating","hypermedia","documents","timed","automata","approach","felix","haeusler","soares"],"keywords":[],"authorIDs":[],"dataSources":["gXSBTZhj3xCWydoZF"]}