检索结果-南通市图书馆

Towards a formal semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2013年第1期28卷 188-202页

作者： Yu Zhou Luciano Baresi Matteo Rossi College of Computer Science Nanjing University of Aeronautics and Astronautics Nanjing 210016 China State Key Laboratory for Novel Software Technology Nanjing University Nanjing 210093 China Department of Electronics and Information Politecnico di Milano Milan 20133 Italy

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.

关键词： timed automata state machine diagram formal semantics

The formal semantics of an UML Activity Diagram

在线全文

学校读者我要写书评

暂无评论

Journal of Shanghai University(English Edition) 2004年第3期8卷 322-327页

作者：梁义芝王延章刘云飞 Institute of Information and Decision Technology Dalian University of Technology Dalian 116024 P.R. China Combat Software Research Center Dalian Naval Academy Dalian 116018 P.R. China Institute of Information and Decision Technology Dalian University of Technology Dalian 116024 P.R. China Education Technology Center Dalian Naval Academy Dalian 116018 P.R. China

Due to lack of strictly defined formal semantics, an UML activity diagram is unsuitable for the tasks of formal analysis, verification and assertion on the system it describes. In this paper, Petri net is used to define the formal semantics of an UML activity diagram containing object flow states, laying a foundation for the precise description and analysis of a workflow system.

关键词： UML activity diagrams formal semantics system analysis.

Event-Based semantics of UML 2.X Concurrent Sequence Diagrams for formal Verification

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2022年第1期37卷 4-28页

作者： Inès Mouakher Fatma Dhaou J.Christian Attiogbé Faculty of Sciences of Tunis University of Tunis El Manar1068TunisTunisia Institute of Technology University of Nantes44322NantesFrance

UML 2.X sequence diagrams(SD)are among privileged scenarios-based approaches dealing with the complexity of modeling the behaviors of some current ***,there are several issues related to the standard semantics of UML 2.X SD proposed by the Object Management Group(OMG).They mainly concern ambiguities of the interpretation of SDs,and the computation of causal relations between events which is not specifically laid ***,SD is a semi-formal language,and it does not support the verification of the modeled *** justifies the considerable number of research studies intending to define formal semantics of UML *** proposed in our previous work semantics covering the most popular combined fragments(CF)of control-flow ALT,OPT,LOOP and SEQ,allowing to model alternative,optional,iterative and sequential behaviors *** proposed semantics is based on partial order theory relations that permit the computation of the precedence relations between the events of an SD with nested *** also addressed the issue of the evaluation of the interaction constraint(guard)for guarded CFs,and the related synchronization *** this paper,we first extend our semantics,proposed in our previous work;indeed,we propose new rules for the computation of causal relations for SD with PAR and STRICT CFs(dedicated to modeling concurrent and strict behaviors respectively)as well as their ***,we propose a transformational semantics in *** modeling approach emphasizes computation of causal relations,guard handling and transformational semantics into *** transformation of UML 2.X SD into the formal method Event-B allows us to perform several kinds of verification including simulation,trace acceptance,verification of properties,and verification of refinement relation between SDs.

关键词： UML 2.X sequence diagram formal semantics nested combined fragment partial order theory Event-B

A novel formal approach to program slicing

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Science in China(Series F) 2007年第5期50卷 657-670页

作者： ZHANG YingZhou College of Computer Nanjing University of Posts and Telecommunications Nanjing 210003 China Institute of Computer Technology Nanjing University of Posts and Telecommunications Nanjing 210003China

Program slicing is a well-known program analysis technique that extracts the elements of a program related to a particular computation. The current slicing methods, however, are singular （mainly based on a program or system dependence graph）, and lack good reusability and flexibility. In this paper, we present a novel formal method for program slicing, modular monadic program slicing, which abstracts the computation of program slicing as a slice monad transformer, and applies it to semantic descriptions of the program analyzed in a modular way, forming the corresponding monadic slicing algorithms. The modular abstraction mechanism allows our slicing method to possess excellent modularity and language-flexibility properties. We also give the related axioms of our slice monad transformer, the proof of the correctness and the implementation of monadic slicing algorithms. We reveal the relations of our algorithms and graph-reachable slicing algorithms.

关键词： program slicing monads modularity slice monad transformer formal semantics

Fuzzy semantics of Contract Language

在线全文

学校读者我要写书评

暂无评论

Applied Mathematics 2016年第5期7卷 422-439页

作者： Hengyang Wu Yixiang Chen Information Engineer College Hangzhou Dianzi University Hangzhou China MoE Engineering Center for Software/Hardware Co-Design Technology and Application

In this paper, we focus on investigation of the predicate transformer semantics of the contract language introduced by Back and von Wright in their book titled as “Refinement Calculus: A Systematic Introduction” (Springer-Verlag, New York, 1998) in the framework of fuzziness. In order to define fuzzy operations, i.e., fuzzy logic connectives, we take into account implicator → and its associated based on residuated lattice theory. Based on these basic fuzzy operations, we introduce the angelic and demonic updates of fuzzy relations. They are the basis of fuzzy predicate transformers in the sense of that any strongly monotone fuzzy predicate transformer can be represented as the sequential composition of the angelic and demonic updates. Together with the standard strong negation , we set up the duality between the angel and demon. The fuzzy predicate transformers semantics of contract statements is established and a simple example of contract statements is given.

关键词： Contract Language formal semantics Residuated Lattice Fuzzy Predicate Transformers

一种基于时序逻辑的UML 2．0形式化语义

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

一种基于时序逻辑的UML 2．0形式化语义

2006年全国理论计算机科学学术年会

作者：黄正宝张广泉苏州大学计算机科学与技术学院苏州大学计算机科学与技术学院

＜正＞1 引言 UML作为一种可视化的建模语言,可以从不同视角描述系统的不同侧面。由于复杂系统的建模往往需要进行严格的形式化分析和验证,而UML 却缺乏精确的形式化语义,限制了它的有效性,因而目前有很多研究UML形式化语义的工作。可执行

关键词： Temporal logic formal semantics UML 2. 0 Sequence diagram State diagram XYZ/E

来源： cnki会议评论

在线全文

cnki会议

学校读者我要写书评

暂无评论

叙事艺术的抒情伦理