One can find various temporal deontic logics in literature, most focusing on discrete time. The literature on real-time constraints and deontic norms is much sparser. Thus, many analysis techniques which have been developed for deontic logics have not been considered for continuous time. In this paper we focus on the notion of conflict analysis which has been extensively studied for discrete time deontic logics. We present a sound, but not complete algorithm for detecting conflicts in timed contract automata and prove the correctness of the algorithm, illustrating the analysis on a case study.

Deontic logics have long been the tool of choice for the formal analysis of normative texts. While various such logics have been proposed many deal with time in a qualitative sense, i.e., reason about the ordering but not timing of events, it was only in the past few years that real-time deontic logics have been developed to reason about time quantitatively. In this paper we present timed contract automata, an automata-based deontic modelling approach complementing these logics with a more operational view of such normative clauses and providing a computational model more amenable to automated analysis and monitoring.

Artificial Intelligence (AI) and the regulation thereof is a topic that is increasingly being discussed and various proposals have been made in literature for defining regulatory bodies and/or related regulation. In this paper, we present a pragmatic approach for providing a technology assurance regulatory framework. To the best of our knowledge, this work presents the first national AI technology assurance legal and regulatory framework that has been implemented by a national authority empowered through law to do so. Aiming to both provide assurances where required and not stifling innovation yet supporting it, it is proposed that such regulation is not to be mandated for all AI-based systems but rather should provide a voluntary framework and only be mandated in sectors and activities as deemed necessary by other authorities or laws for regulated and critical areas.

One advantage of using formal deontic logic to represent and reason about normative texts is that one can analyse such texts in a precise and incontrovertible manner. Conflict analysis is one such analysis technique — assessing whether a number of contracts, or more generally normative texts, are internally consistent, in that they may not lead to a situation in which active norms conflict or even contradict each other. In this paper we extend existing techniques from the literature to address conflicts in the context of environmental constraints on actions regulated by the contract, and which the parties involved can carry out. The approach is logic-agnostic and we show how it can be applied to a service provision contract written in 𝒞ℒ.

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.

Smart contracts have been proposed as executable implementations enforcing real-life contracts. Unfortunately, the semantic gap between these allows for the smart contract to diverge from its intended deontic behaviour. In this paper we show how a deontic contract can be used for real-time monitoring of smart contracts specifically and request-based interactive systems in general, allowing for the identification of any violations. The deontic logic of actions we present takes into account the possibility of action failure (which we can observe in smart contracts), allowing us to consider novel monitorable semantics for deontic norms. For example, taking a rights-based view of permissions allows us to detect the violation of a permission when a permitted action is not allowed to succeed. A case study is presented showing this approach in action for Ethereum smart contracts.

Despite that many real-life contracts include time constraints, for instance explicitly specifying deadlines by when to perform actions, or for how long certain behaviour is prohibited, the literature formalising such notions is surprisingly sparse. Furthermore, one of the major challenges is that compliance is typically computed with respect to timed event traces with event timestamps assumed to be perfect. In this paper we present an approach for evaluating compliance under the effect of imperfect timing information, giving a semantics to analyse contract violation likelihood.

User interfaces which adapt based on usage patterns, for example based on frequency of use of certain features, have been proposed as a means of limiting the complexity of the user interface without specialising it unnecessarily to particular user profiles. However, from a software engineering perspective, adaptive user interfaces pose a challenge in code structuring, and separation of the different layers of user interface and application state and logic can introduce interdependencies which make software development and maintenance more challenging. In this paper we explore the use of monitoring-oriented programming to add adaptive features to user interfaces, an approach which has been touted as a means of separating certain layers of logic from the main system. We evaluate the approach both using standard software engineering measures and also through a user acceptance experiment - by having a number of developers use the proposed approach to add adaptation logic to an existing application.

Static verification techniques are used to analyse and prove properties about programs before they are executed. Many of these techniques work directly on the source code and are used to verify data-oriented properties over all possible executions. The analysis is necessarily an over-approximation as the real executions of the program are not available at analysis time. In contrast, runtime verification techniques have been extensively used for control-oriented properties, analysing the current execution path of the program in a fully automatic manner. In this article, we present a novel approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language we present to achieve this that of ppDATEs, which enhances the control-oriented property language of DATEs, with data-oriented pre/postconditions. For runtime verification of ppDATE specifications, the language is translated into a DATE. We give a formal semantics to ppDATEs, which we use to prove the correctness of our translation from ppDATEs to DATEs. We show how ppDATE specifications can be analysed using a combination of the deductive theorem prover KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY first partially proves the data-oriented part of the specification, simplifying the specification which is then passed on to LARVA to check at runtime for the remaining parts of the specification including the control-oriented aspects. We show the applicability of our approach on two case studies.

Natural language techniques have been employed in attempts to automatically translate legal texts, and specifically contracts, into formal models that allow automatic reasoning. However, such techniques suffer from incomplete coverage, typically resulting in parts of the text being left uninterpreted, and which, in turn, may result in the formal models failing to identify potential problems due to these unknown parts. In this paper we present a formal approach to deal with partiality, by syntactically and semantically permitting unknown subcontracts in an action-based deontic logic, with accompanying formal analysis techniques to enable reasoning under incomplete knowledge.

Defining and characterising conditional permissions has never been easy. Part of the problem, we believe, comes from the fact that there is not one but a whole family of possible deontic operators, all of them distinct and reasonable, that can be labelled as conditional permissions. In this article, rather than disputing the correct interpretation, we revisit a number of different interpretations the term has received in the literature, and propose appropriate formalisations for these interpretations within the context of contract automata.

Although contract reparations have been extensively studied in the context of deontic logics, there is not much literature using reparations in automata-based deontic approaches. Contract automata is a recent approach to modelling the notion of contract-based interaction between different parties using synchronous composition. However, it lacks the notion of reparations for contract violations. In this article we look into, and contrast different ways reparation can be added to an automaton- and state-based contract approach, extending contract automata with two forms of such clauses: catch-all reparations for violation and reparations for specific violations.

In regulated interactive systems, one party's behaviour may impose restrictions on how others may behave when interacting with it. These restrictions may be seen as implicit contracts which the affected party has to conform to and may thus be considered inappropriate or excessive if they overregulate one of the parties. In this paper we characterise such implicit contracts and present an algorithmic way of synthesising them using a formalism based on contract automata to regulate interactive action-based systems.

We present a formalization of Kanger's types of rights in the context of interacting two-party systems, such as contracts. We show that in this setting basic rights such as claim, freedom, power and immunity can be expressed in terms of (possibly negated) permissions and obligations over presence or absense of actions. Another way of saying this is that, at least in the context of contracts, neither claim, nor power, nor freedom nor immunity are foundational modalities, as they can be defined in terms of others. We also show that the set of atomic type rights is different from Kanger's original proposal.

Despite the fact that contracts are, by definition, an agreement between two or more parties, most formal studies limit themselves to contracts regulating only a single party or the parties independently of each other, without looking into how permissions, obligations or prohibitions of one party affect the other. This article deals with the analysis of what different types of permissions mean in the context of contracts. To give formal semantics we use an automata based formalism allowing to model for one party agreeing, delaying or plain refusing on performing certain actions that the other is attempting. This approach also yields a natural notion of contract strictness analysis for each party.

The use of runtime verification, as a lightweight approach to guarantee properties of systems, has been increasingly employed on real-life software. In this paper, we present the tool LARVA, for the runtime verification of properties of Java programs, including real-time properties. Properties can be expressed in a number of notations, including timed-automata enriched with stopwatches, Lustre, and a subset of the duration calculus. The tool has been successfully used on a number of case-studies, including an industrial system handling financial transactions. LARVA also performs analysis of real-time properties, to calculate, if possible, an upper-bound on the memory and temporal overheads induced by monitoring. Moreover, through property analysis, LARVA assesses the impact of slowing down the system through monitoring, on the satisfaction of the properties.