The Formal Semantics of an UML Activity Diagram

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.

Fuzzy Semantics of Contract Language

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.

Trust Management Mechanism for Internet of Things

Trust management has been proven to be a useful technology for providing security service and as a consequence has been used in many applications such as P2P, Grid, ad hoc network and so on. However, few researches about trust mechanism for Internet of Things （IoT） could be found in the literature, though we argue that considerable necessity is held for applying trust mechanism to IoT. In this paper, we establish a formal trust management control mechanism based on architecture modeling of IoT. We decompose the IoT into three layers, which are sensor layer, core layer and application layer, from aspects of network composition of loT. Each layer is controlled by trust management for special purpose： self-organized, affective routing and multi-service respectively. And the final decision-making is performed by service requester according to the collected trust information as well as requester＇ policy. Finally, we use a formal semantics-based and fuzzy set theory to realize all above trust mechanism, the result of which provides a general framework for the development of trust models of IoT.

A Comparative Typological Study of Italian and Georgian Jargon Words

Italian youth speak their own language.The language used by youth can be considered a special language.Italian youth language has different functions.The functions which should be distinguished are:entertainment,expression,identity,and secrecy.Today,jargon has the function of entertainment more than that of secrecy.In Georgia,jargon has always been considered a foul and vulgar language.Georgian jargon words are less common than Italian ones.Georgian jargon has become popular recently.The material reviewed in the paper includes 2,700 items taken from dictionaries and the Internet.We divided them into two thematic groups:(1)related to everyday life;and(2)related to vicious aspects of life.The first group includes topics,such as money,work,the police,and youth discourse.The second group includes theft,drugs,sex life,and alcohol.The aim of this paper is to conduct a comparative study of groups of jargon identified as a result of thematic classification,in terms of methods of word formation.The study will allow us to identify semantic and formal methods of jargon word formation applied in these two unrelated languages,as well as similarities and differences between Italian and Georgian jargon words and phraseological units.

Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata

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.

Event-Based Semantics of UML 2.X Concurrent Sequence Diagrams for Formal Verification

UML 2.X sequence diagrams(SD)are among privileged scenarios-based approaches dealing with the complexity of modeling the behaviors of some current systems.However,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 out.Moreover,SD is a semi-formal language,and it does not support the verification of the modeled system.This justifies the considerable number of research studies intending to define formal semantics of UML SDs.We 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 respectively.The 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 CFs.We also addressed the issue of the evaluation of the interaction constraint(guard)for guarded CFs,and the related synchronization issue.In 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 nesting.Then,we propose a transformational semantics in Event-B.Our modeling approach emphasizes computation of causal relations,guard handling and transformational semantics into Event-B.The 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.

A Formal Semantics for DAI Language NUML

Traditional AI systems are brittle in the sense that they fail miserably whenpresented with problems even slightly outside of their limited range of expertise.A powerful, extensible strategy of Distributed Artificial Intelligence (DAI) forovercoming such bounds is to put the system in a society of systems. So theability to coordinate group activities of individuals and to communicate betweeneach other is necessary for a language describing DAI systems. Agent-orientedlanguage NUML is such a language. It is a specific kind of object-orientedlanguage. To give formal semantics to NUML, there is the problem to for-malise object-oriented programming paradigm which is still open. The theoryof higher-order rr-calculus is a concurrent computation model with sufficientcapability, which provides us a mathematical tool to do the formalization. Thispaper tries to use higher-order T-calculus to formalise NUML.

Metadata as a Methodological Commons:From Aboutness Description to Cognitive Modeling

Metadata is data about data,which is generated mainly for resources organization and description,facilitating finding,identifying,selecting and obtaining information.With the advancement of technologies,the acquisition of metadata has gradually become a critical step in data modeling and function operation,which leads to the formation of its methodological commons.A series of general operations has been developed to achieve structured description,semantic encoding and machine-understandable information,including entity definition,relation description,object analysis,attribute extraction,ontology modeling,data cleaning,disambiguation,alignment,mapping,relating,enriching,importing,exporting,service implementation,registry and discovery,monitoring etc.Those operations are not only necessary elements in semantic technologies(including linked data)and knowledge graph technology,but has also developed into the common operation and primary strategy in building independent and knowledge-based information systems.In this paper,a series of metadata-related methods are collectively referred to as'metadata methodological commons',which has a lot of best practices reflected in the various standard specifications of the Semantic Web.In the future construction of a multi-modal metaverse based on Web 3.0,it shall play an important role,for example,in building digital twins through adopting knowledge models,or supporting the modeling of the entire virtual world,etc.Manual-based description and coding obviously cannot adapted to the UGC(User Generated Contents)and AIGC(AI Generated Contents)-based content production in the metaverse era.The automatic processing of semantic formalization must be considered as a sure way to adapt metadata methodological commons to meet the future needs of Al era.

A novel formal approach to program slicing

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.