scholarly journals From parametric trace slicing to rule systems

2021 ◽  
Author(s):  
Giles Reger ◽  
David Rydeheard
Keyword(s):  
Runtime Verification ◽  
Specification Languages ◽  
Execution Traces ◽  
Running System ◽  
Proof Of Correctness ◽  
Rule Systems ◽  
The Relationship ◽  
Specification Techniques ◽  
Previous Conference

AbstractParametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper continues our work exploring the relationship between specification techniques for parametric runtime verification. Here we consider the correspondence between trace-slicing automata-based approaches and rule systems. The main contribution is a translation from quantified automata to rule systems, which has been implemented in Scala. This then allows us to highlight the key differences in how the two formalisms handle data, an important step in our wider effort to understand the correspondence between different specification languages for parametric runtime verification. This paper extends a previous conference version of this paper with further examples, a proof of correctness, and an optimisation based on a notion of redundancy observed during the development of the translation.

Runtime Verification on Robotics Systems

2015 ◽  
Vol 3 (1) ◽  
pp. 23-40 ◽  
Author(s):  
Zhijiang Dong ◽  
Yujian Fu ◽  
Yue Fu
Keyword(s):  
Embedded Systems ◽  
Formal Method ◽  
Mobile Apps ◽  
Runtime Verification ◽  
Software Quality Assurance ◽  
Execution Traces ◽  
On Line ◽  
Implementation Level ◽  
Automatic Technique

Runtime verification is a technique for generating monitors from formal specification of expected behaviors for the underlying system. It can be applied to automatically evaluate system execution, either on-line or off-line, analyzing extracted execution traces; or it can be used online during operation, potentially steering the application back to a safety region if a property is violated. As a so-called light-weighted formal method, runtime verification bridges the gap between system design and implementation and shorten the distance of software quality assurance between the software testing and model checking and theorem proving. Runtime verification is considered as a highly scalable and automatic technique. Most of current runtime verification research are endeavored on the program context, in other words, on the program side and falls in the implementation level. These applications limited the benefits of runtime verification that bridges the gap among types of applications. With the proliferation of embedded systems and mobile device, dynamically verifying the firmware and mobile apps becomes a new emerging area. Due to the characteristics of runtime verification technique and limitations of the robotics systems, so far, very few research and project are located in the runtime verification on the firmware of embedded systems, which appear in most of robotics systems. Robotics systems are programmed on the firmware and only observed on device. In this paper, the authors first discussed the current runtime verifications on the embedded systems with limitations. After that, a layered runtime verification framework will be presented for the firmware verification. The case study is applied on the commonly recognized educational toolkit – LEGO Mindstorm robotics systems.

The optimal community detection of software based on complex networks

2016 ◽  
Vol 27 (08) ◽  
pp. 1650085 ◽  
Author(s):  
Guoyan Huang ◽  
Peng Zhang ◽  
Bing Zhang ◽  
Tengteng Yin ◽  
Jiadong Ren
Keyword(s):  
Community Structure ◽  
Design Patterns ◽  
Execution Traces ◽  
Dependency Relationship ◽  
Software Network ◽  
Close Relationship ◽  
Dependency Network ◽  
Software Execution ◽  
Maintenance Process ◽  
The Relationship

The community structure is important for software in terms of understanding the design patterns, controlling the development and the maintenance process. In order to detect the optimal community structure in the software network, a method Optimal Partition Software Network (OPSN) is proposed based on the dependency relationship among the software functions. First, by analyzing the information of multiple execution traces of one software, we construct Software Execution Dependency Network (SEDN). Second, based on the relationship among the function nodes in the network, we define Fault Accumulation (FA) to measure the importance of the function node and sort the nodes with measure results. Third, we select the top K(K=1,2,…) nodes as the core of the primal communities (only exist one core node). By comparing the dependency relationships between each node and the K communities, we put the node into the existing community which has the most close relationship. Finally, we calculate the modularity with different initial K to obtain the optimal division. With experiments, the method OPSN is verified to be efficient to detect the optimal community in various softwares.

scholarly journals Rule Systems for Runtime Verification: A Short Tutorial

2009 ◽  
pp. 1-24 ◽  
Author(s):  
Howard Barringer ◽  
Klaus Havelund ◽  
David Rydeheard ◽  
Alex Groce
Keyword(s):  
Runtime Verification ◽  
Rule Systems

Débrouillardise: certifying ‘conflict-free’ minerals in a context of regulatory pluralism in South Kivu, DR Congo

2015 ◽  
Vol 53 (2) ◽  
pp. 145-168 ◽  
Author(s):  
Marie Müller-Koné
Keyword(s):  
Gold Mining ◽  
Legal Status ◽  
Ad Hoc ◽  
Transnational Governance ◽  
Mining Sites ◽  
Republic Of The Congo ◽  
South Kivu ◽  
Rule Systems ◽  
The Relationship ◽  
Free Status

AbstractThis article explores the relationship between transnational governance initiatives for ‘conflict-free’ certification in the eastern provinces of the Democratic Republic of the Congo (DRC) and the regulatory pluralism one finds on the ground. Efforts in certifying artisanal gold mining are scrutinised by analysing how three different gold mining sites in the DRC's South Kivu province are governed. Most artisanal mining in the DRC is usually referred to as ‘informal’ – a term associated with non-state actors. Instead, the article introduces the idea of a mode of governing that follows the principle of ‘débrouillardise’, which combines different rule systems and state and non-state regulators. It argues that ‘conflict-free’ governance will need to improvise viaad hocagreements on the legal status of mining sites among state authorities, economic actors and international monitors. The act of declaring mining sites legal will provide for the semblance of a ‘conflict-free’ status and a unitary state system of rule, while in practice, the plurality of regulatory authority will not be reversed.

scholarly journals CASL for CafeOBJ Users

2000 ◽  
Vol 7 (51) ◽  
Author(s):  
Peter D. Mosses
Keyword(s):  
Research And Development ◽  
Expressive Language ◽  
Software Requirements ◽  
Future Research ◽  
Algebraic Specification ◽  
Main Stream ◽  
Collaborative Effort ◽  
Specification Languages ◽  
Common Framework ◽  
The Relationship

Casl is an expressive language for the algebraic specification<br />of software requirements, design, and architecture. It has been developed by an open collaborative effort called CoFI (Common Framework Initiative for algebraic specification and development). Casl combines the best features of many previous main-stream algebraic specification languages, and it should provide a focus for future research and development in the use of algebraic techniques, as well facilitating interoperability of<br />existing and future tools. This paper presents Casl for users of the CafeOBJ framework, focusing on the relationship between the two languages. It first considers those constructs of CafeOBJ that have direct counterparts in Casl, and then (briefly) those that do not. It also motivates various Casl constructs<br />that are not provided by CafeOBJ. Finally, it gives a concise overview of Casl, and illustrates how some CafeOBJ specifications may be expressed in Casl.

scholarly journals A survey of challenges for runtime verification from advanced application domains (beyond software)

2019 ◽  
Vol 54 (3) ◽  
pp. 279-335 ◽  
Author(s):  
César Sánchez ◽  
Gerardo Schneider ◽  
Wolfgang Ahrendt ◽  
Ezio Bartocci ◽  
Domenico Bianculli ◽  
...  
Keyword(s):  
Dynamic Analysis ◽  
Formal Methods ◽  
Computational Models ◽  
State Of The Art ◽  
Runtime Verification ◽  
Formal Specifications ◽  
New Techniques ◽  
Execution Traces ◽  
Current State ◽  
Potential Applications

Abstract Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.

The Protection of Intellectual Property in International Law

2017 ◽  
Author(s):  
Henning Grosse Ruse-Khan
Keyword(s):  
Intellectual Property ◽  
International Law ◽  
Free Trade ◽  
Legal System ◽  
Biological Diversity ◽  
Ip Protection ◽  
Holistic View ◽  
Ip Law ◽  
Rule Systems ◽  
The Relationship

This book examines intellectual property (IP) protection in the broader context of international law. Against the background of the debate about norm relations within and between different rule systems in international law, it constructs a holistic view of international IP law as an integral part of the international legal system. The first part considers norm relations within the international IP law system. It analyses the relationship of the two main unilateral IP conventions to the World Trade Organisation (WTO) Agreement on Trade Related Aspects of International Property Rights (TRIPS), as well as the relationship between TRIPS and subsequent Free Trade Agreements (FTAs). The second part discusses alternative rule systems for the protection of IP. The third part identifies important intersections and links between the traditional system of IP protection and other areas of international law related to environmental, social, and economic concerns. These include free trade in goods; biological diversity, genetic resources, and traditional knowledge; multilateral environmental agreements (MEAs) on climate change; and access to medicines and food. This analysis provides significant insights into the nature and quality of international law as a legal system. The fourth part identifies appropriate norms within the international IP system that can respond to these complexities and linkages.

scholarly journals Commuting Double Sugeno Integrals

2019 ◽  
Vol 27 (Supp01) ◽  
pp. 1-38
Author(s):  
Didier Dubois ◽  
Hélène Fargier ◽  
Agnès Rico
Keyword(s):  
Expected Utility ◽  
Two Dimensions ◽  
The Other ◽  
Decision Problems ◽  
One Dimension ◽  
Two Dimensional ◽  
Conference Paper ◽  
The Relationship ◽  
Previous Conference

In decision problems involving two dimensions (like several agents in uncertainty) the properties of expected utility ensure that the result of a two-stepped procedure evaluation does not depend on the order with which the aggregations of local evaluations are performed (e.g., agents first, uncertainty next, or the converse). We say that the aggregations on each dimension commute. In a previous conference paper, Ben Amor, Essghaier and Fargier have shown that this property holds when using pessimistic possibilistic integrals on each dimension, or optimistic ones, while it fails when using a pessimistic possibilistic integral on one dimension and an optimistic one on the other. This paper studies and completely solves this problem when more general Sugeno integrals are used in place of possibilistic integrals, leading to double Sugeno integrals. The results show that there are capacities other than possibility and necessity measures that ensure commutation of Sugeno integrals. Moreover, the relationship between two-dimensional capacities and the commutation property for their projections is investigated.

Interstellar gas in the central region of the Galaxy

1967 ◽  
Vol 31 ◽  
pp. 239-251 ◽  
Author(s):  
F. J. Kerr
Keyword(s):  
Central Region ◽  
Galactic Plane ◽  
Neutral Hydrogen ◽  
Continuum Emission ◽  
Galactic Centre ◽  
Interstellar Gas ◽  
Hydrogen Recombination ◽  
The Galaxy ◽  
Centre Region ◽  
The Relationship

A review is given of information on the galactic-centre region obtained from recent observations of the 21-cm line from neutral hydrogen, the 18-cm group of OH lines, a hydrogen recombination line at 6 cm wavelength, and the continuum emission from ionized hydrogen.Both inward and outward motions are important in this region, in addition to rotation. Several types of observation indicate the presence of material in features inclined to the galactic plane. The relationship between the H and OH concentrations is not yet clear, but a rough picture of the central region can be proposed.

The relationship of the scleractinian corals to the rugose corals

Paleobiology ◽  
1980 ◽  
Vol 6 (02) ◽  
pp. 146-160 ◽  
Author(s):  
William A. Oliver
Keyword(s):  
Critical Points ◽  
Scleractinian Corals ◽  
Convincing Evidence ◽  
Early Triassic ◽  
Rugose Corals ◽  
History Of ◽  
The Subject ◽  
Relationship Of ◽  
The Relationship ◽  
Biologic Factors

The Mesozoic-Cenozoic coral Order Scleractinia has been suggested to have originated or evolved (1) by direct descent from the Paleozoic Order Rugosa or (2) by the development of a skeleton in members of one of the anemone groups that probably have existed throughout Phanerozoic time. In spite of much work on the subject, advocates of the direct descent hypothesis have failed to find convincing evidence of this relationship. Critical points are:(1) Rugosan septal insertion is serial; Scleractinian insertion is cyclic; no intermediate stages have been demonstrated. Apparent intermediates are Scleractinia having bilateral cyclic insertion or teratological Rugosa.(2) There is convincing evidence that the skeletons of many Rugosa were calcitic and none are known to be or to have been aragonitic. In contrast, the skeletons of all living Scleractinia are aragonitic and there is evidence that fossil Scleractinia were aragonitic also. The mineralogic difference is almost certainly due to intrinsic biologic factors.(3) No early Triassic corals of either group are known. This fact is not compelling (by itself) but is important in connection with points 1 and 2, because, given direct descent, both changes took place during this only stage in the history of the two groups in which there are no known corals.

Sign in / Sign up

Export Citation Format

Share Document