Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFormal Modelling of Ontologies : An Event-B based Approach Using the Rodin Platform
116
0
0.0
(
0
)
Added by
EPTCS
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Authors
Yamine Ait Ameur
Ask ChatGPT about the research
No Arabic abstract
This paper reports on the results of the French ANR IMPEX research project dealing with making explicit domain knowledge in design models. Ontologies are formalised as theories with sets, axioms, theorems and reasoning rules. They are integrated to design models through an annotation mechanism. Event-B has been chosen as the ground formal modelling technique for all our developments. In this paper, we particularly describe how ontologies are formalised as Event-B theories.
rate research
Read More
Problems faced by international standardization bodies become more and more crucial as the number and the size of the standards they produce increase. Sometimes, also, the lack of coordination among the committees in charge of the development of standards may lead to overlaps, mistakes or incompatibilities in the documents. The aim of this study is to present a methodology enabling an automatic extraction of the technical concepts (terms) found in normative documents, through the use of semantic tools coming from the field of language processing. The first part of the paper provides a description of the standardization world, its structure, its way of working and the problems faced; we then introduce the concepts of semantic annotation, information extraction and the software tools available in this domain. The next section explains the concept of ontology and its potential use in the field of standardization. We propose here a methodology enabling the extraction of technical information from a given normative corpus, based on a semantic annotation process done according to reference ontologies. The application to the ISO 15531 MANDATE corpus provides a first use case of the methodology described in this paper. The paper ends with the description of the first experimental results produced by this approach, and with some issues and perspectives, notably its application to other standards and, or Technical Committees and the possibility offered to create pre-defined technical dictionaries of terms.
In cloud computing, software-defined network (SDN) gaining more attention due to its advantages in network configuration to improve network performance and network monitoring. SDN addresses an issue of static architecture in traditional networks by allowing centralised control of a network system. SDN contains centralised network intelligence module which separates a process of forwarding packets (data plane) from packet routing process (control plane). It is essential to ensure the correctness of SDN due to secure data transmitting in it. In this paper. Model-checking is chosen to verify an SDN network. The Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) used as a specification to express properties of an SDN. Then complete SDN structure is defined formally along with its Kripke structure. Finally, temporal properties are analysed against the SDN Kripke model to assure the properties of SDN is correct.
For large-scale distributed systems, its crucial to efficiently diagnose the root causes of incidents to maintain high system availability. The recent development of microservice architecture brings three major challenges (i.e., operation, system scale, and monitoring complexities) to root cause analysis (RCA) in industrial settings. To tackle these challenges, in this paper, we present Groot, an event-graph-based approach for RCA. Groot constructs a real-time causality graph based on events that summarize various types of metrics, logs, and activities in the system under analysis. Moreover, to incorporate domain knowledge from site reliability engineering (SRE) engineers, Groot can be customized with user-defined events and domain-specific rules. Currently, Groot supports RCA among 5,000 real production services and is actively used by the SRE teamin a global e-commerce system serving more than 185 million active buyers per year. Over 15 months, we collect a data setcontaining labeled root causes of 952 real production incidents for evaluation. The evaluation results show that Groot is able to achieve 95% top-3 accuracy and 78% top-1 accuracy. To share our experience in deploying and adopting RCA in industrial settings, we conduct survey to show that users of Grootfindit helpful and easy to use. We also share the lessons learnedfrom deploying and adopting Grootto solve RCA problems inproduction environments.
Player experience (PX) evaluation has become a field of interest in the game industry. Several manual PX techniques have been introduced to assist developers to understand and evaluate the experience of players in computer games. However, automated testing of player experience still needs to be addressed. An automated player experience testing framework would allow designers to evaluate the PX requirements in the early development stages without the necessity of participating human players. In this paper, we propose an automated player experience testing approach by suggesting a formal model of event-based emotions. In particular, we discuss an event-based transition system to formalize relevant emotions using Ortony, Clore, & Collins (OCC) theory of emotions. A working prototype of the model is integrated on top of Aplib, a tactical agent programming library, to create intelligent PX test agents, capable of appraising emotions in a 3D game case study. The results are graphically shown e.g. as heat maps. Emotion visualization of the test agent would ultimately help game designers in creating content that evokes a certain experience in players.
Formal Methods tools will never have as many users as tools for popular programming languages and so the effort spent on constructing Integrated Development Environments (IDEs) will be orders of magnitudes lower than that of programming languages such as Java. This means newcomers to formal methods do not get the same user experience as with their favourite programming IDE. In order to improve this situation it is essential that efforts are combined so it is possible to reuse common features and thus not start from scratch every time. This paper presents the Overture platform where such a reuse philosophy is present. We give an overview of the platform itself as well as the extensibility principles that enable much of the reuse. The paper also contains several examples platform extensions, both in the form of new features and a new IDE supporting a new language.
suggested questions
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
