SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.
Citation: | Yu Zhou, Luciano Baresi, Matteo Rossi. Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata[J]. Journal of Computer Science and Technology, 2013, 28(1): 188-202. DOI: 10.1007/s11390-013-1322-8 |
[1] |
OMG. UML profile for MARTE: Modeling and analysis ofreal-time embedded systems. Version 1.0, formal/2009-11-02,2009, http://www.omg.org/spec/MARTE/1.0/.
|
[2] |
Baresi L, Pezze M. On formalizing UML with high-level Petrinets. In Concurrent Object-Oriented Programming and PetriNets, Springer Verlag, 2001, pp.276-304.
|
[3] |
Crane M, Dingel J. Towards a formal account of a foundationalsubset for executable UML models. In Proc. the 11thInternational Conference on Model Driven Engineering Languagesand Systems, October 2008, pp.675-689.
|
[4] |
David A, Möller M, Yi W. Formal verification of UML statechartswith real-time extensions. In Proc. the 5th Int.Conf. Fundamental Approaches to Software Engineering,Apr. 2002, pp.218-232.
|
[5] |
Latella D, Majzik I, Massink M. Towards a formal operationalsemantics of UML statechart diagrams. In Proc. the3rd International Conference on Formal Methods for OpenObject-Based Distributed Systems, March 1999, p.465.
|
[6] |
Andr′e C, Mallet F, Peraldi-Frati M. A multiform time approachto real-time system modeling: Application to an automotivesystem. In Proc. the International Symposium onIndustrial Embedded Systems, July 2007, pp.234-241.
|
[7] |
Mallet F, de Simone F. MARTE: A profile for RT/E systemsmodeling, analysis-and simulation? In Proc. the 1st Simutools,June 2008, Article No.43.
|
[8] |
OMG. UML profile for MARTE: Modeling and analysis ofreal-time embedded systems. Version 1.1, formal/2011-06-02,2011, http://www.omg.org/spec/MARTE/1.1.
|
[9] |
Alur R, Dill D. A theory of timed automata. TheoreticalComputer Science, 1994, 126(2): 183-235.
|
[10] |
Berthomieu B, Ribet P, Vernadat F. The tool TINA-Construction of abstract state spaces for petri nets and timepetri nets. International Journal of Production Research,2004, 42(14): 2741-2756.
|
[11] |
Fecher H, Schönborn J, Kyas M, de Roever W. 29 new unclaritiesin the semantics of UML 2.0 state machines. In Proc. the7th International Conference on Formal Methods and SoftwareEngineering, November 2005, pp.52-65.
|
[12] |
OMG. OMG unified modeling languageTM (OMG UML), superstructure.Version 2.2, 2009, http://www.omg.org/spec/UML/2.2/Superstructure.
|
[13] |
Mikk E, Lakhnechi Y, Siegel M. Hierarchical automata asmodel for statecharts. In Proc. the 3rd Asian Computing ScienceConf. Advance in Computing Science, December 1997,pp.181-196.
|
[14] |
Behrmann G, David A, Larsen K. A tutorial on UPPAAL. InProc. the International Conference on Formal Methods forthe Design of Real-time Systems, July 2004, pp.33-35.
|
[15] |
Lamport L. Time, clocks, and the ordering of events in a distributedsystem. Communications of the ACM, 1978, 21(7):558-565.
|
[16] |
Mallet F, Andr′e C. On the semantics of UML/MARTEclock constraints. In Proc. the Int. Symp.Object/Component/Service-Oriented Real-Time DistributedComputing, Mar. 2009, pp.305-312.
|
[17] |
Ge N, Pantel M. Time properties dedicated semantics forUML-MARTE safety critical real-time system verification. InProc. the 8th European Conference on Modelling Foundationsand Applications, July 2012, pp.25-39.
|
[18] |
Crane M, Dingel J. On the semantics of UML state machines:Categorization and comparision. Technical Report 2005-501,Queen’s University, 2005.
|
[19] |
Harel D, Naamad A. The STATEMATE semantics of statecharts.ACM Transactions on Software Engineering andMethodology, 1996, 5(4): 293-333.
|
[20] |
David A, Möller M. From HUPPAAL to UPPAAL: A translationfrom hierarchical timed automata to flat timed automata.Technical Report, University of Aarhus, 2001.
|
[21] |
Giese H, Burmester S. Real-time statechart semantics. TechnicalReport TR-RI-03-239, University of Paderborn, 2003.
|
[22] |
Akshay S, Bollig B, Gastin P, Mukund M, Kumar K N. Distributedtimed automata with independently evolving clocks.In Proc. the 19th International Conference on ConcurrencyTheory, August 2008, pp.82-97.
|
[23] |
Hu Z, Shatz S. Explicit modeling of semantics associated withcomposite states in UML statecharts. Automated SoftwareEngineering, 2006, 13(4): 423-467.
|
[24] |
Hölscher K, Ziemann P, GogollaM. On translating UML modelsinto graph transformation systems. Journal of Visual Languages& Computing, 2006, 17(1): 78-105.
|
[25] |
Kong J, Zhang K, Dong J, Xu D. Specifying behavioral semanticsof UML diagrams through graph transformations.Journal of Systems and Software, 2009, 82(2): 292-306.
|
[26] |
Bindelli S, Di Nitto E, Furia C et al. Using compositionalityto formally model and analyze systems built of a high numberof components. In Proc. the 15th Int. Conf. Eng. ofComplex Computer Systems, Mar. 2010, pp.85-94.
|
[1] | Yuan Li, Xing-Chen Wang, Lin Huang, Yun-Lei Zhao. Order-Revealing Encryption: File-Injection Attack and Forward Security[J]. Journal of Computer Science and Technology, 2021, 36(4): 877-895. DOI: 10.1007/s11390-020-0060-y |
[2] | Yan-Hong Fan, Mei-Qin Wang, Yan-Bin Li, Kai Hu, Mu-Zhou Li. A Secure IoT Firmware Update Scheme Against SCPA and DoS Attacks[J]. Journal of Computer Science and Technology, 2021, 36(2): 419-433. DOI: 10.1007/s11390-020-9831-8 |
[3] | Qi-Qi Lai, Bo Yang, Yong Yu, Zhe Xia, Yan-Wei Zhou, Yuan Chen. Updatable Identity-Based Hash Proof System Based on Lattices and Its Application to Leakage-Resilient Public-Key Encryption Schemes[J]. Journal of Computer Science and Technology, 2018, 33(6): 1243-1260. DOI: 10.1007/s11390-018-1885-5 |
[4] | Jing Xu, Wen-Tao Zhu. A Generic Framework for Anonymous Authentication in Mobile Networks[J]. Journal of Computer Science and Technology, 2013, 28(4): 732-742. DOI: 10.1007/s11390-013-1371-z |
[5] | Yan Zhu, Hong-Xin Hu, Gail-Joon Ahn, Huai-Xi Wang, Shan-Biao Wang. Provably Secure Role-Based Encryption with Revocation Mechanism[J]. Journal of Computer Science and Technology, 2011, 26(4): 697-710. DOI: 10.1007/s11390-011-1169-9 |
[6] | Hai-Bo Tian, Willy Susilo, Yang Ming, Yu-Min Wang. A Provable Secure ID-Based Explicit Authenticated Key Agreement Protocol Without Random Oracles[J]. Journal of Computer Science and Technology, 2008, 23(5): 832-842. |
[7] | Yong-Dong Zhang, Sheng Tang, Jin-Tao Li. Secure and Incidental Distortion Tolerant Digital Signature for Image Authentication[J]. Journal of Computer Science and Technology, 2007, 22(4): 618-625. |
[8] | Sin-Kyu Kim, Jae-Woo Choi, Dae-Hun Nyang, Gene-Beck Hahn, Joo-Seok Song. Smart Proactive Caching Scheme for Fast Authenticated Handoff in Wireless LAN[J]. Journal of Computer Science and Technology, 2007, 22(3): 476-480. |
[9] | Qing-Hua Zheng, David L. Pepyne, Qing Wang. New Approach to WLAN Security with Synchronized Pseudo Random[J]. Journal of Computer Science and Technology, 2004, 19(6). |
[10] | ZHENG Dong, CHEN Kefei, YOU Jinyuan. Multiparty Authentication Services and Key Agreement Protocols with Semi-Trusted Third Party[J]. Journal of Computer Science and Technology, 2002, 17(6). |