{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T08:18:39Z","timestamp":1676449119714},"reference-count":8,"publisher":"World Scientific Pub Co Pte Lt","issue":"02","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2005,4]]},"abstract":"<jats:p> This contribution proposes a link between the specification of supervisory controllers by Sequential Function Charts (SFC) and the verification of embedded systems with hybrid dynamics. The SFC are transformed into modular timed automata using a procedure based on graph grammars. The resulting controller model is composed with a hybrid automaton (with possibly nonlinear continuous dynamics) that models the plant behavior. In order to verify safety properties of the composed system algorithmically, a tool implementing the recently proposed approach of counterexample guided model checking is employed. The procedure is illustrated for a processing system example. <\/jats:p>","DOI":"10.1142\/s021819400500204x","type":"journal-article","created":{"date-parts":[[2005,5,24]],"date-time":"2005-05-24T07:56:24Z","timestamp":1116921384000},"page":"307-312","source":"Crossref","is-referenced-by-count":9,"title":["VERIFICATION OF EMBEDDED SUPERVISORY CONTROLLERS CONSIDERING HYBRID PLANT DYNAMICS"],"prefix":"10.1142","volume":"15","author":[{"given":"SEBASTIAN","family":"ENGELL","sequence":"first","affiliation":[{"name":"Process Control  Laboratory (BCI-AST), University of Dortmund,  44221 Dortmund, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"SVEN","family":"LOHMANN","sequence":"additional","affiliation":[{"name":"Process Control  Laboratory (BCI-AST), University of Dortmund,  44221 Dortmund, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"OLAF","family":"STURSBERG","sequence":"additional","affiliation":[{"name":"Process Control  Laboratory (BCI-AST), University of Dortmund,  44221 Dortmund, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf2","doi-asserted-by":"publisher","DOI":"10.1016\/S0098-1354(00)00484-1"},{"key":"rf3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-4493-7_25"},{"key":"rf4","doi-asserted-by":"crossref","unstructured":"P.\u00a0L'Her, P.\u00a0Le Parc and L.\u00a0Marce, Automata Implementation, LNCS\u00a01660 (Springer, Berlin, 1998)\u00a0pp. 149\u2013163.","DOI":"10.1007\/3-540-48057-9_13"},{"key":"rf6","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410300190X"},{"key":"rf9","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2004.04.002"},{"key":"rf10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27863-4_22"},{"key":"rf12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36580-X_35"},{"key":"rf13","doi-asserted-by":"publisher","DOI":"10.3166\/ejc.7.361-381"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S021819400500204X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T12:17:10Z","timestamp":1565180230000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S021819400500204X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,4]]},"references-count":8,"journal-issue":{"issue":"02","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2005,4]]}},"alternative-id":["10.1142\/S021819400500204X"],"URL":"https:\/\/doi.org\/10.1142\/s021819400500204x","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,4]]}}}