The China-Europe International Symposium on Software Engineering Education(CEISEE)is an international educational conference jointly initiated by Harbin Institute of Technology and Technological University Dublin in 2...The China-Europe International Symposium on Software Engineering Education(CEISEE)is an international educational conference jointly initiated by Harbin Institute of Technology and Technological University Dublin in 2005.The CEISEE is held alternately in China and Europe every year.The host cities include Harbin,Dublin in Ireland,Guangzhou,Bordeaux in France,Xi’an,Northampton in the United Kingdom,Shanghai,Milan in Italy,Chengdu,Zwikau in Germany,Shenyang,Athens in Greece,Shenzhen,Lisbon in Portugal,Beijing,and Wuhan in 2023.The conference has been gaining increasing international influence.展开更多
UML is a widely-used, general purpose modeling language. But its lack of a rigorous semantics forbids the thorough analysis of designed solution, and thus precludes the discovery of significant problems at design time...UML is a widely-used, general purpose modeling language. But its lack of a rigorous semantics forbids the thorough analysis of designed solution, and thus precludes the discovery of significant problems at design time. To bridge the gap, the paper investigates the underlying semantics of UML state machine diagrams, along with the time-related modeling elements of MARTE, the profile for modeling and analysis of real-time embedded systems, and proposes a formal operational semantics based on extended hierarchical timed automata. The approach is exemplified on a simple example taken from the automotive domain. Verification is accomplished by translating designed models into the input language of the UPPAAL model checker.展开更多
文摘The China-Europe International Symposium on Software Engineering Education(CEISEE)is an international educational conference jointly initiated by Harbin Institute of Technology and Technological University Dublin in 2005.The CEISEE is held alternately in China and Europe every year.The host cities include Harbin,Dublin in Ireland,Guangzhou,Bordeaux in France,Xi’an,Northampton in the United Kingdom,Shanghai,Milan in Italy,Chengdu,Zwikau in Germany,Shenyang,Athens in Greece,Shenzhen,Lisbon in Portugal,Beijing,and Wuhan in 2023.The conference has been gaining increasing international influence.
基金This work was supported by the European Community 7th Framework Program （FP7/2007-2013） under Grant agreement No. 248864 （MADES） and the National Natural Science Foundation of China under Grant No. 61202002.
文摘UML is a widely-used, general purpose modeling language. But its lack of a rigorous semantics forbids the thorough analysis of designed solution, and thus precludes the discovery of significant problems at design time. To bridge the gap, the paper investigates the underlying semantics of UML state machine diagrams, along with the time-related modeling elements of MARTE, the profile for modeling and analysis of real-time embedded systems, and proposes a formal operational semantics based on extended hierarchical timed automata. The approach is exemplified on a simple example taken from the automotive domain. Verification is accomplished by translating designed models into the input language of the UPPAAL model checker.
