Search

Future unmanned aircraft systems are allowed to incorporate operational aspects for flight approval due to the new EASA “specific” category. Incorporating operational aspects offer new possibilities for the verification and validation of complex functions used especially in highly automated vehicles. For these functions, verification and validation can focus on predefined operational aspects prior to flight. In-flight, limits of the operation are monitored to assure the correct working environment for these functions resulting in a safe operation. In this paper, we present the notion of safe operation monitoring and depict operational limits to be supervised. One prominent example for such an operational limit is geofencing. Geofencing prevents an unmanned aircraft from entering a forbidden airspace by using virtual fences. Specifically, in this paper, we present an algorithm and describe parameters for the buffer distance used for the geofence boundary values. The algorithm can be highly parallelized which is important when considering realistic geofences of future operations. Further, we highlight the use of a formal specification language and simulation results which support the verification and validation of geofencing, respectively. The chosen specification language is not limited to geofencing, other operational limits can be expressed and monitored in-flight to assure the safe operation.

Runtime verification allows validation of systems during their operation by monitoring crucial system properties. It is common to generate monitors from temporal specifications formulated in languages like MTL or LTL. However, writing formal specifications might be an obstacle for practitioners. In this paper we present an approach and a tool for generating software monitors for reactive systems from a set of Generalized Test Tables (GTTs)—a table-based, user-friendly specification language specially designed for engineers. The tool is a valuable addition to the already existing static verifier for GTTs since assumptions made in specifications can thus be validated at runtime. Moreover, it makes software and specifications amenable for formal validation that cannot be verified statically. Moreover, the approach is particularly well-suited for the specification of workflows as a collection of tables since it supports dynamic, trigger-based spawning of monitors. The tool produces monitor code in C++ for tables provided in an existing table definition format. We show the usefulness of our approach using characteristic examples.

We present the design of a framework to describe parametrized exercise tasks on Haskell-I/O programming. Parametrized tasks can be instantiated randomly to quickly generate different instances of a task. Such automatic task generation is useful in many different ways. Manual task creation can be a time-consuming process, so formulating a task design once and then automatically generating different variations can save valuable time for the educator. The descriptions of tasks also serve as easy to understand documentation and can be reused in new task designs. On the student’s side automatic task generation, together with an automated assessment system, enables practicing on as many fresh exercise tasks as needed. Students can also each be given a slightly different version of tasks, reducing issues regarding plagiarism arising naturally in an e-learning environment. Our task generation is centered around a specification language for I/O behavior we developed in earlier work. The task generation framework, an embedded domain specific language in Haskell, provides powerful primitives for the creation of various artifacts from specifications, including program code. We do not go into detail on the technical realization of these primitives. Our focus is on showcasing how such artifacts can be used as an alternative to the verbal description of requirements for different types of programming exercise tasks. By doing so, we are able to automatically generate a diverse range of task designs.

The article presents a comprehensive approach to solving a number of problems that arise during the design, development, debugging and maintenance of multicomponent applications. The approach is based on a created formalism that allows specifying the structure and visible behavior of the component external to the application. At the same time, the mathematical approach used in the formalism is based on the system of extended finite state machine, which allows analyzing specifications in an acceptable time. For a programmer to set formal descriptions of the components, the LibSL specification language is developed. It allows the programmer to describe the specification of a component or a library in the form that is understandable to the programmer, without going into the mathematical basics of formalism. In this case, the interface of the library and its behavior, which is visible from the outside, are set. The implementation details are not included in the specification.

This paper reports on the current state of the DEMO Specification Language (DEMOSL). The Design and Engineering Methodology for Organisations (DEMO) is a principal methodology in Enterprise Engineering (EE), while the DEMOSL defines the accompanying integrated modelling landscape.

Traditionally, graph algorithms get a single graph as input, and then they should decide if this graph satisfies a certain property \(\varPhi \). What happens if this question is modified in a way that we get a possibly infinite family of graphs as an input, and the question is if there exists one graph satisfying \(\varPhi \)? We approach this question by using formal languages for specifying families of graphs. In particular, we show that certain graph properties can be decided by studying the syntactic monoid of the specification language.

Unit testing frameworks are nowadays considered a best practice, foregone in almost all modern software development processes, to achieve rapid development of correct specifications. The first unit testing specification language for Answer Set Programming (ASP) was proposed in 2011 as a feature of the ASPIDE development environment. Later, a more portable unit testing language was included in the LANA annotation language. In this paper we propose a revisited unit testing specification language that allows one to inline tests within ASP program and an ASP-based test execution mechanism. Moreover, we present a programming environment supporting test driven development (TDD) of ASP programs with our language.

The domain of Subject-oriented Business Process Management (S-BPM) is somewhat outstanding due to its embracing of Subject Orientation. However, at the same time, it is also a classic BPM domain concerned with typical aspects like creation and exchange of diagrammatic process models, elicitation of domain knowledge, and implementing process (models) into organisations and IT systems. Nevertheless, the Abstract State Machine (ASM) concept, a formal and abstract specification means for algorithms, has been and is fundamental and an important cornerstone for the S-BPM community. The first formal specifications for S-BPM has been developed by Egon Borger using ASM means—namely a specification for an interpreter engine for the subject-oriented modeling language PASS, the Parallel Activity Specification Schema. However, for the sake of intuitive and comprehensive use, ASM can be enriched with defining the passive aspects of PASS, namely the (data) structure of process models and data object appearing in the processes. Here it is useful to complement ASM description means with concepts that are better suited for that tasks. This work analyzes how the S-BPM research community has combined ASM with the Web Ontology Language (OWL) to generate a precise, while comprehensible, system specification for the execution of formal, subject-oriented process models. Furthermore, it will be argued why this combination is worthwhile overcoming the weaknesses of both generic and technology independent specification approaches.

In the health sector, data analysis is typically performed by specialty using clinical data stored in a Clinical Data Registry (CDR), specific to that medical specialty. Therefore, if we want to analyze data from a new specialty, it is necessary to create a new CDR, which is usually done from scratch. Although the data stored in CDRs depends on the medical specialty, typically data has a common structure and the operations over it are similar (e.g., entering and viewing patient data). These characteristics make the creation of new CDRs possible to automate. In this paper, we present a software system for automatic CDR generation, called CDRGen, that relies on a metadata specification language to describe the data to be collected and stored, and the types of supported users as well as their permissions for accessing data. CDRGen parses the input specification language and generates the code needed for a functional CDR. The specification language is defined on top of a metamodel that describes the metadata of a generic CDR. The metamodel was designed taking into account the analysis of eleven existing CDRs. The experimental assessment of the CDRGen indicates that: (i) developers can create new CDRs more efficiently (in less than 2% of the typical time), (ii) CDRGen creates the user interface functionalities to enter and access data and the database to store that data, and finally, (iii) its specification language has a high expressiveness enabling the inclusion of a large variety of data types. Our solution will help developers creating new CDRs for different specialties in a fast and easy way, without the need to create everything from scratch.

Social dependance relationships were used in the i* requirements modelling language to represent dependencies among social actors. We study the evolution of the notion of social dependency into that of commitment in the Azzurra specification language for business processes, and then into the notions of obligation and power in the Symboleo specification language for legal contracts. Our account focuses on the difference in the semantics of these relationships, the language used to talk about them, and how appropriate they are for capturing requirements for services.

State-based formal specifications benefit from data structuring mechanisms, which collate associated properties and efficiently declare complex types. For example, ‘record’ data structures, similar to those used in programming languages, can be built into the concrete syntax of a language as an enhancement over flat data relationships. While this is relatively simple to achieve for a single-level specification, it becomes significantly more involved when the specification language allows for progressive refinement of the data supporting the specification. Individual fields may be added to create sub-records within a refinement and replaced to create refined records during a refinement step. The impact on the ability to verify invariant and refinement proof obligations must be considered. Here we describe a record structuring syntax that includes notions of extension and inheritance that can be used in a refinement-based formal method. We illustrate the approach using extensions to the Event-B formal method.

Nowadays, information systems (IS) are making considerable efforts to create, develop, and build new and more advanced models capable of modeling all (or the mainstream) development trends in IS. The progress in IS is mainly related to three main points: document-centered approaches, modern database management systems and their applications, and new flexible models, which are more complex than existing models in most cases. The challenges of the modeling process are mainly the presentation of both the static and dynamic sides of the developed IS. The latter is directly influenced by the change processes of the business environment. In this paper, we use the properties of the Activity Diagram, represented by Alloy - an operationalizable specification language for software architecture - together with the underlying mathematical model to simplify the semantics of the models and to facilitate their analysis, verification, and validation.

Formal verification of real-life industrial software remains a challenging task. It provides strong guarantees of correctness, which are particularly important for security-critical products, such as smart cards. Security of a smart card strongly relies on the requirement that the underlying JavaCard virtual machine ensures necessary isolation properties. This case study paper presents a recent formal verification of a JavaCard Virtual Machine implementation performed by Thales using the Frama-C verification toolset. This is the first verification project for such a large-scale industrial smart card product where deductive verification is applied on the real-life C code. The target properties include common security properties such as integrity and confidentiality. The implementation contains over 7,000 lines of C code. After a formal specification in the ACSL specification language, over 52,000 verification conditions were generated and successfully proved. We present several issues identified during the project, illustrate them by representative examples and present solutions we used to solve them. Finally, we describe proof results, some lessons learned and desired tool improvements.

In this paper we discuss our method on applying the ArchiMate modelling language for specification in the context of Big Data applications. The DataBio project [1] develops the pilot applications for bioeconomy industry by applying Big Data technologies. The project regroups 26 pilots from 17 different countries to be implemented and deployed with more than 40 components and services. The choice of ArchiMate [2] is motivated by the need to express the overall business context of each pilot in conjunction with the technical architecture for possible solutions from various perspectives. The ArchiMate bridges the gap between those perspectives and can serve as an input for the model-driven development of Big Data applications. The authors provide the essence of the method and illustrate it with an example.

This paper describes the formalisation of SGAC access control policies using Z3 and then we compare the performance with ProB and Alloy. SGAC is an attribute-based, fine-grain access control model that uses acyclic subject and resource graphs to provide rule inheritance and streamline policy specification. To ensure patient privacy and safety, four types of properties are checked: accessibility, availability, contextuality and rule effectiveness. Automatic translation of SGAC policies into each specification language has been defined. ProB offers the best verification performances, by two orders of magnitude. The performances of Alloy and Z3 are similar.

Alloy is a lightweight specification language based on relational logic, with an analysis engine that relies on SAT solvers to automate bounded verification of specifications. In spite of its strengths, the reliance of the Alloy Analyzer on computationally heavy solvers means that it can take a significant amount of time to verify software properties, even within limited bounds. This challenge is exacerbated by the ever-evolving nature of complex software systems. This paper presents Platinum, a technique for efficient analysis of evolving Alloy specifications, that recognizes opportunities for constraint reduction and reuse of previously identified constraint solutions. The insight behind Platinum is that formula constraints recur often during the analysis of a single specification and across its revisions, and constraint solutions can be reused over sequences of analyses performed on evolving specifications. Our empirical results show that Platinum substantially reduces (by 66.4% on average) the analysis time required on specifications extracted from real-world software systems.

The MU theory or EE model theory is a theory of models and modelling in general, and of conceptual modelling in particular. The foundations part starts with this definition of model: any subject using a system A to obtain knowledge of a system B is using A as a model of B. It conveys clearly the basic understanding of the concept of model as a role notion. Next, the model triangle is introduced, based on the semiotic triangle from the FI theory. It clarifies how complexes (systems and aggregates) of three major sorts (concrete, conceptual, and symbolic) can be used as models of each other. By adding two levels of abstraction (namely the schema level and the meta level), the General Conceptual Modelling Framework emerges. It clarifies the notions of conceptual complex, conceptual schema, and meta schema for any Universe of Discourse or system’s world. It is also made clear that these notions are logical constructs, and that consequently any expression of them (in a suitable language) is directly transformable to first-order logic. The elaborations part comprises the presentation and discussion of the General Ontology Specification Language (GOSL). GOSL is a universal language for specifying conceptual complexes, conceptual schemas, and meta schemas. The syntax of the language consists of graphical as well as textual symbols and constructs. The latter constitute an English-like formal language. The split between the two is a pragmatic one. Compared to common graphical languages for conceptual modelling, GOSL might be called minimal: it covers only the basic concepts and constructs. More complicated logical formulas can often be better expressed in textual constructs. The discussions part starts with a comparison of the GCMF with two other frameworks. Next, the influence of O-O thinking on conceptual modelling is discussed. It appears that O-O thinking causes the blurring of two crucial things in conceptual modelling: the type–instance relationship and the subtype–supertype relationship.

Linear logic and its refinements have been used as a specification language for a number of deductive systems. This has been accomplished by carefully studying the structural restrictions of linear logic modalities. Examples of such refinements are subexponentials, light linear logic, and soft linear logic. We bring together these refinements of linear logic in a non-commutative setting. We introduce a non-commutative substructural system with subexponential modalities controlled by a minimalistic set of rules. Namely, we disallow the contraction and weakening rules for the exponential modality and introduce two primitive subexponentials. One of the subexponentials allows the multiplexing rule in the style of soft linear logic and light linear logic. The second subexponential provides the exchange rule. For this system, we construct a sequent calculus, establish cut elimination, and also provide a complete focused proof system. We illustrate the expressive power of this system by simulating Turing computations and categorial grammar parsing for compound sentences. Using the former, we prove undecidability results. The new system employs Lambek’s non-emptiness restriction, which is incompatible with the standard (sub)exponential setting. Lambek’s restriction is crucial for applications in linguistics: without this restriction, categorial grammars incorrectly mark some ungrammatical phrases as being correct.

In this chapter DEMO (Design and Engineering Methodology for Organisations) is presented, in order to produce the essential model of an enterprise, or in general of a Scope of Interest (which may cover a part of one enterprise or of a network of enterprises). Like every proper methodology, DEMO comprises a Way of Thinking (WoT), a Way of Modelling (WoM), and a Way of Working (WoW). The WoT consists of the theories that are discussed in part B of this book. The WoM consists of an integrated whole of four aspect models: the Cooperation model (CM), the Action Model (AM), the Process Model (PM), and the Fact Model (FM). The CM of a Scope of Interest (SoI) is the ontological model of its construction, thus of the identified transactor roles and the coordination structures among them. Three structures are distinguished: the interaction structure, the interimpediment structure and the interstriction structure. The AM of an SoI is the ontological model of its operation. For every internal actor role, it provides the rules that guide the role fillers in doing their work. The guidelines for responding to coordination events are called action rules (similar to business rules), the ones for performing production acts are called work instructions. The PM of an SoI is the ontological model of the state space and the transition space of its coordination world. It contains the existence laws and occurrence laws for all internal and border transactor roles. The PM connects the CM and the AM of an SoI as far as coordination is concerned. The FM of an SoI is the ontological model of the state space and the transition space of its production world. It contains the existence laws and occurrence laws for all identified entity types, value types, property types, attribute types, and event types. The PM connects the CM and the AM of an SoI as far as production is concerned. All four sub-models are expressed in the DEMO Specification Language (DEMOSL), which comprises diagrams, tables, and formal textual descriptions. For producing essential models of enterprises, the WoW of DEMO offers the OER method (Organisational Essence Revealing). It consists of a number of steps in which the four aspect models are produced, preferably in a spiral way.

International audience; We present an automated workflow for the analysis of multi-agent systems described in a simple specification language. The procedure is based on a structural encoding of the input system and the property of interest into an LNT program, and relies on the CADP software toolbox to either verify the given property or simulate the encoded system. Counterexamples to properties under verification, as well as simulation traces, are translated into a syntax similar to that of the input language: therefore, no knowledge of CADP is required. The workflow is implemented as a module of the verification tool SLiVER. We present the input specification language, describe the analysis workflow, and show how to invoke SLiVER to verify or simulate two example systems. Then, we provide details on the LNT encoding and the verification procedure.

Behavioral synthesis is a technique that automatically builds a controller for a system given its specification. This is achieved by obtaining a winning strategy in a game between the system and the environment. Behavioral synthesis has been successfully applied in modern modularization techniques such as Aspect Orientation to compose each particular view of the system in a single piece. When a controller can not be found the engineer faces the Non Realizability Problem. In this work we exploit FVS a distinguishable feature in the FVS specification language called anti-scenarios to address this problem. Several case studies are introduced to show our proposal in action. Additionally, a performance analysis is introduced to further validate our approach.

The Linux kernel is one of the most important Free/Libre Open Source Software (FLOSS) projects. It is installed on billions of devices all over the world, which process various sensitive, confidential or simply private data. It is crucial to establish and prove its security properties. This work-in-progress paper presents a method to verify the Linux kernel for conformance with an abstract security policy model written in the Event-B specification language. The method is based on system call tracing and aims at checking that the results of system call execution do not lead to accesses that violate security policy requirements. As a basis for it, we use an additional Event-B specification of the Linux system call interface that is formally proved to satisfy all the requirements of the security policy model. In order to perform the conformance checks we use it to reproduce intercepted system calls and verify accesses.

As part of the design of a space mission, an important part is the design of so-called flight rules. Flight rules express constraints on various parts and processes of the mission, that if followed, will reduce the risk of failure. One such set of flight rules constrain the format of command sequences regularly (e.g. daily) sent to the spacecraft to control its next near term behavior. We present a high-level view of the automated flight rule checker Frc for checking command sequences sent to NASA’s LADEE Lunar mission spacecraft, used throughout its entire mission. A command sequence is in this case essentially a program (a sequence of commands) with no loops or conditionals, and it can therefore be verified with a trace analysis tool. Frc is implemented using the TraceContract runtime verification tool, an internal Scala DSL for checking event sequences against “formal specifications”. The paper illustrates this untraditional use of runtime verification in a real context, with strong demands on the expressiveness and flexibility of the specification language, illustrating the advantages of an internal DSL.

Constraints are an important aspect of role-based access control management (RBAC). Constraints have to be satisfied in user—role assignment and permission—role assignment. The importance of constraints associated with user-role assignments and permission-role assignments in RBAC has been recognized but the modelling of these constraints has not received much attention. In this chapter we use a de facto constraints specification language in software engineering to analyze the constraints in user-role assignments and permission-role assignments. Object Constraints Language (OCL), a part of the Unified Modelling Language (UML) widely used in object-oriented analysis and design is applied to express various constraints in RBAC. We analyse elements, relationships, constraints and structure of RBAC adopting class diagram method in UML. Then the representations of role-based access constraints such as separation, prerequisite, cardinality and mobility constraints with OCL are identified. Finally, comparisons with other related work and our future work are presented.

Runtime monitors that are specified in a stream-based monitoring language tend to be easier to understand, maintain, and reuse than those written in a standard programming language. Because of their formal semantics, such specification languages are also a natural choice for safety-critical applications. Unlike for standard programming languages, there is, however, so far very little support for automatic code optimization. In this paper, we present the first collection of code transformations for the stream-based monitoring language RTLola. We show that classic compiler optimizations, such as Sparse Conditional Constant Propagation and Common Subexpression Elimination, can be adapted to monitoring specifications. We also develop new transformations -- Pacing Type Refinement and Filter Refinement -- which exploit the specific modular structure of RTLola as well as the implementation freedom afforded by a declarative specification language. We demonstrate the significant impact of the code transformations on benchmarks from the monitoring of unmanned aircraft systems (UAS).

Developing cloud-native applications demands a radical shift from the way we design and build traditional applications. Application designers usually divide their business logic into several business functions, each developed according to a microservices architectural style and packaged in containers. Throughout the stages of cloud-native application development (development, testing, staging and production), container orchestration helps coordinate the execution environment. Thanks to the increasing popularity of cloud-native applications, there has been a growing interest in container and orchestration technologies recently. However, despite their closeness, these two inter-related technologies are supported by different toolsets and specification formalisms, with minimal portability between them and usually a disregard for the best practices. This paper presents velo, a domain-specific language (DSL) that unifies containerisation and orchestration concepts. velo has two components: (1) a specification language that supports an abstract description of containerisation and orchestration for a complex application; and (2) a transpiler, a source-to-source compiler into concrete container manifest and orchestration description.

Formal method is an important approach to develop high trust software systems. Coq is an interactive proof assistant for the development of mathematical theories and formally certified software. Set, Bag, List, Tree, Graph are important reusable components in PAR platform. This paper tries to formally develop ‘Set’ components which have linear structure and verify the correctness of this component mechanically with Coq. The formal development of this component involves formalization of specification, the recurrence relation of problem-solving sequence and loop invariant. Specification language Radl of PAR platform was used to describe the specification, recurrence relation and loop invariants; Software modelling language Apla was used to describe the abstract model of those components. The Dijkstra’s Weakest Precondition method is used to verify abstract model by the interactive proof tool Coq. Finally, the abstract model denoted by Apla was transformed to concrete model written by executable language; such as C++, Java, VB and C#, etc., based on the program generating systems in PAR platform.

International audience; In this paper, we study the semantics of a specification language for the coordination of concurrent systems, which supports time at different levels: various time domains, polychrony, and mixed metric/logical time constraints. The language itself is defined by a denotational semantics. In order to be able to construct the possible timelines for verification purposes, we also define a symbolic operational semantics, which is the reference for an efficient implementation of a tool for runtime-testing of heterogeneous systems. This study presents a novel way to link these two semantics by taking advantage of a coinductive unfolding principle of these timelines. Furthermore, these semantics and their equivalence have been formalized in the Isabelle/HOL proof assistant, together with proofs for soundness, completeness and progress.

The autonomous control of unmanned aircraft is a highly safety-critical domain with great economic potential in a wide range of application areas, including logistics, agriculture, civil engineering, and disaster recovery. We report on the development of a dynamic monitoring framework for the DLR ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) family of unmanned aircraft based on the formal specification language RTLola. RTLola is a stream-based specification language for real-time properties. An RTLola specification of hazardous situations and system failures is statically analyzed in terms of consistency and resource usage and then automatically translated into an FPGA-based monitor. Our approach leads to highly efficient, parallelized monitors with formal guarantees on the noninterference of the monitor with the normal operation of the autonomous system.

Software applications have been developed with multiple programming languages (specific software libraries and frameworks) and deployed on various software and hardware infrastructures. This paper introduces and discusses- the ASL language (short for “Application Specification Language”) that combines constructs from two previous languages: ITLingo RSL and IFML. ASL specifications are strict and rigorous sentences that allow us to define both requirements and user interfaces aspects of software applications in a consistent and integrated way. Alike RSL, and differently from IFML, ASL is a controlled natural language with a textual concrete syntax. Furthermore, the proposed approach includes model-to-model and model-to-code transformations that may considerably improve the quality and productivity of both the requirements specification and the development of software applications.

Signal temporal logic (STL) and reachability analysis are effective mathematical tools for formally analyzing the behavior of robotic systems. STL is a specification language that uses logic and temporal operators to precisely express real-valued and time-dependent requirements on system behaviors. While recursively defined STL specifications are extremely expressive and controller synthesis methods exist, there has not been work that quantifies the set of states from which STL formulas can be satisfied. Reachability analysis, on the other hand, involves computing the reachable set – the set of states from which a system is able to reach a goal while satisfying state and control constraints. While reasoning about system requirements through sets of states is useful for predetermining the possibility of satisfying desired system properties and obtaining state feedback controllers, so far the application of reachability has been limited to reach-avoid specifications. In this paper, we merge STL and time-varying reachability into a single framework that combines the key advantage of both methods – expressiveness of specifications and set quantification. To do this, we establish a correspondence between temporal and reachability operators, and use the idea of least-restrictive feasible controller sets (LRFCSs) to break down controller synthesis for complex STL formulas into a sequence of reachability and elementary set operations. LRFCSs are crucial for avoiding controller conflicts among different reachability operations. In addition, the synthesized state feedback controllers are guaranteed to satisfy STL specifications if determined to be possible by our framework, and violate specifications minimally if not. For simplicity, Hamilton-Jacobi reachability will be used in this paper, although our method is agnostic to the time-varying reachability method. We demonstrate our method through numerical simulations and robotic experiments.

Code generation is gaining popularity as a technique to bridge the gap between high-level models and executable code. We describe the theory underlying the PVS2C code generator that translates functional programs written using the PVS specification language to standalone, efficiently executable C code. We outline a correctness argument for the code generator. The techniques used are quite generic and can be applied to transform programs written in functional languages into imperative code. We use a formal model of reference counting to capture memory management and safe destructive updates for a simple first-order functional language with arrays. We exhibit a bisimulation between the functional execution and the imperative execution. This bisimulation shows that the generated imperative program returns the same result as the functional program.

This paper describes a method of computing plausible states of a system as a logical model. The problem of analyzing state-based systems as they evolve over time has been studied widely in the automated reasoning community (and others). This paper proposes a specific approach, one that is tailored to situational awareness applications. The main contribution is a calculus for a novel specification language that is built around disjunctive logic programming under a possible models semantics, stratification in terms of event times, default negation, and a model revision operator for dealing with incomplete or erroneous events – a typical problem in realistic applications. The paper proves the calculus correct wrt. a formal semantics of the specification language and it describes the calculus’ implementation via embedding in Scala. This enables immediate access to rich data structures and external systems, which is important in practice.

Cryptographic protocols are an important part of any protected system. Verifying their security is an important task to ensure the security of such systems. To enable security analysis, various verifiers are used. To do this, it is necessary to describe the protocol in specific specification languages, specify the verification objectives, and then directly conduct a security analysis. The paper presents a general approach for translating the presentation of the protocol from the Alice-Bob form to any specification language. The main elements allocated for the protocol when describing it in the specification language are given. Roles, data transmission channels, initial knowledge of roles, model of an attacker, initial knowledge of an attacker, message transfer are highlighted. A description of the CAS+ specification language for use in the Avispa verifier is provided. The algorithm for translating the Alice-Bob view to the CAS+ specification is given. An algorithm is presented for both automated verification of the protocol originally described in the Alice-Bob format and partially automated using the Avispa graphical interface. An example of the operation of the translation algorithm and automated verification is shown.