Search

Alternating timed automata (ATA) are an extension of timed automata, that are closed under complementation and hence amenable to logic-to-automata translations. Several timed logics, including Metric Temporal Logic (MTL), can be converted to equivalent 1-clock ATAs (1-ATAs). Satisfiability of an MTL formula therefore reduces to checking emptiness of a 1-ATA. Furthermore, algorithms for 1-ATA emptiness can be adapted for model-checking timed automata models against 1-ATA specifications. However, existing emptiness algorithms for 1-ATA proceed by an extended region construction, and are not suitable for implementations. In this work, we improve the existing MTL-to-1-ATA construction and develop a zone based emptiness algorithm for 1-ATAs. We first introduce a deactivation operation on the 1-ATA syntax to allow an explicit deactivation of the clock in transitions. Using the deactivation operation, we improve the existing MTL-to-1-ATA conversion and present a fragment of MTL for which the equivalent 1-ATA generate a bounded number of variables. Secondly, we develop the idea of zones for 1-ATA and present an emptiness algorithm which explores a corresponding zone graph. For termination, a special entailment check between zones is necessary. Our main technical contributions are: (1) an algorithm for the entailment check using simple zone operations and (2) an NP-hardness for the entailment check in the general case. Finally, for 1-ATA which generate a bounded number of variables, we present a modified entailment check with quadratic complexity., Comment: A shorter version appears in FoSSaCS 2025

Abstract: Failing test case reduction can promote efficient debugging because a developer may not need to observe components that are not relevant to inducing failure. Failing test case reduction can also improve the efficiency of fault localization. These considerations have prompted researchers to study the reduction process, the reduction output, and the removed entities. Christi et al. studied test reduction using a tool called ReduSharptor for C# tests. They considered the test to be an Abstract Syntax Tree (AST). Based on that, they studied the reduction outcome and removed entities in terms of Leaf nodes and Non-Leaf nodes of the AST. They claimed that (1) leaf nodes are removed in large numbers, and (2) the probability of removal is slightly higher than non-leaf nodes. We replicate their results using a different test case reduction tool, ReduJavator, for Java unit tests. We evaluate test reduction using 30 randomly chosen bugs from the Defects4J database and 30 mutants for 6 open-source projects. Our results confirm their first claim: leaf nodes are removed in large numbers. Our results are inconclusive regarding their second claim; we cannot confirm that the probability of removal is higher for non-leaf nodes., Comment: 5 pages and 4 figures

Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps underlying the verdict in an exchangeable format, enabling independent validation of the reasoning by other tools. For the correctness of concurrent programs, no agreed-upon witness format exists -- in no small part due to the divide between the semantics considered by analyzers, ranging from interleaving to thread-modular approaches, making it challenging to exchange information. We propose a format that leverages the well-known notion of ghosts to embed the claims a tool makes about a program into a modified program with ghosts, such that the validity of a witness can be decided by analyzing this program. Thus, the validity of witnesses with respect to the interleaving and the thread-modular semantics coincides. Further, thread-modular invariants computed by an abstract interpreter can naturally be expressed in the new format using ghost statements. We evaluate the approach by generating such ghost witnesses for a subset of concurrent programs from the SV-COMP benchmark suite, and pass them to a model checker. It can confirm 75% of these witnesses -- indicating that ghost witnesses can bridge the semantic divide between interleaving and thread-modular approaches., Comment: 38 pages

Digitalization efforts often face a key challenge: business processes must not only be efficient in achieving their goals but also adhere to legal regulations. Business process compliance refers to aligning processes with these regulations. Numerous frameworks have been developed to address this, with the earliest dating back to 1981. This study focuses on rigorous frameworks using formal methods to verify or ensure compliance. We conducted a systematic literature review (SLR) on process compliance frameworks based on formal models. Our goal was to assess the current state of research on process model compliance and identify gaps and opportunities for future work. Starting with 5018 candidate studies from 1981 to the establishment of GDPR, we selected 46 primary studies. These frameworks were categorized by their phases, the languages used for processes and compliance, and their reasoning techniques. We also examined their practical applicability, the case studies they were tested on, the types of users involved, and the skills needed for compliance. Also, we assessed the maturity of each framework. Our findings reveal strong consensus around verification techniques as central to process compliance, though there is less agreement on the earlier and later phases of compliance. Model checking is the dominant technique, but the compliance and process languages have evolved. Most frameworks are still conceptual with prototype implementations, often failing to account for compliance professionals like legal experts or law changes. In conclusion, there is a need for comprehensive empirical studies to better understand the anatomy and maturity of regulatory compliance frameworks, and for robust evaluation methods to benchmark these frameworks. This review offers valuable insights for researchers and practitioners in process compliance., Comment: 39 pages, 16 Figures, 12 tables

Intelligent Cyber-Physical Systems (ICPS) represent a specialized form of Cyber-Physical System (CPS) that incorporates intelligent components, notably Convolutional Neural Networks (CNNs) and Deep Reinforcement Learning (DRL), to undertake multifaceted tasks encompassing perception, decision-making, and control. The utilization of DRL for decision-making facilitates dynamic interaction with the environment, generating control actions aimed at maximizing cumulative rewards. Nevertheless, the inherent uncertainty of the operational environment and the intricate nature of ICPS necessitate exploration within complex and dynamic state spaces during the learning phase. DRL confronts challenges in terms of efficiency, generalization capabilities, and data scarcity during decision-making process. In response to these challenges, we propose an innovative abstract modeling approach grounded in spatial-temporal value semantics, capturing the evolution in the distribution of semantic value across time and space. A semantics-based abstraction is introduced to construct an abstract Markov Decision Process (MDP) for the DRL learning process. Furthermore, optimization techniques for abstraction are delineated, aiming to refine the abstract model and mitigate semantic gaps between abstract and concrete states. The efficacy of the abstract modeling is assessed through the evaluation and analysis of the abstract MDP model using PRISM. A series of experiments are conducted, involving diverse scenarios such as lane-keeping, adaptive cruise control, and intersection crossroad assistance, to demonstrate the effectiveness of our abstracting approach., Comment: 24 pages, 7 figures, conference

Isabelle2Cpp is a code generation framework that supports automatic generation of C++ code from Isabelle/HOL specifications. However, if some type information of Isabelle/HOL specification is missing, Isabelle2Cpp may not complete the code generation automatically. In order to solve this problem, this paper provides a type system for Isabelle2Cpp, which is used to perform type inference and type unification for expressions of the intermediate representation in Isabelle2Cpp. The system introduces new type inference rules and unification algorithms to enhance the Isabelle2Cpp framework. By incorporating the type system, the Isabelle2Cpp framework can provide more comprehensive type information for expression generation, which leads to more complete and accurate C++ code., Comment: 22 pages, 4 figures

We discuss what is special about the reproducibility of workflows in computer algebra. It is emphasized how the programming language Julia and the new computer algebra system OSCAR support such a reproducibility, and how users can benefit for their own work., Comment: 15 pages

Software Engineering (SE) Pre-trained Language Models (PLMs), such as CodeBERT, are pre-trained on large code corpora, and their learned knowledge has shown success in transferring into downstream tasks (e.g., code clone detection) through the fine-tuning of PLMs. In Natural Language Processing (NLP), an alternative in transferring the knowledge of PLMs is explored through the use of adapter, a compact and parameter efficient module that is inserted into a PLM. Although the use of adapters has shown promising results in many NLP-based downstream tasks, their application and exploration in SE-based downstream tasks are limited. Here, we study the knowledge transfer using adapters on multiple down-stream tasks including cloze test, code clone detection, and code summarization. These adapters are trained on code corpora and are inserted into a PLM that is pre-trained on English corpora or code corpora. We called these PLMs as NL-PLM and C-PLM, respectively. We observed an improvement in results using NL-PLM over a PLM that does not have adapters, and this suggested that adapters can transfer and utilize useful knowledge from NL-PLM to SE tasks. The results are sometimes on par with or exceed the results of C-PLM; while being more efficient in terms of the number of parameters and training time. Interestingly, adapters inserted into a C-PLM generally yield better results than a traditional fine-tuned C-PLM. Our results open new directions to build more compact models for SE tasks., Comment: Accepted to EMSE

Decentralised Finance (DeFi) applications constitute an entire financial ecosystem deployed on blockchains. Such applications are based on complex protocols and incentive mechanisms whose financial safety is hard to determine. Besides, their adoption is rapidly growing, hence imperilling an increasingly higher amount of assets. Therefore, accurate formalisation and verification of DeFi applications is essential to assess their safety. We have developed a tool for the formal analysis of one of the most widespread DeFi applications: Lending Pools (LP). This was achieved by leveraging an existing formal model for LPs, the Maude verification environment and the MultiVeStA statistical analyser. The tool supports several analyses including reachability analysis, LTL model checking and statistical model checking. In this paper we show how the tool can be used to analyse several parameters of LPs that are fundamental to assess and predict their behaviour. In particular, we use statistical analysis to search for threshold and reward parameters that minimize the risk of unrecoverable loans.

The goal of the DARPA Automated Rapid Certification Of Software (ARCOS) program is to "automate the evaluation of software assurance evidence to enable certifiers to determine rapidly that system risk is acceptable." As part of this program, the DesCert project focuses on the assurance-driven development of new software. The DesCert team consists of SRI International, Honeywell Research, and the University of Washington. We have adopted a formal, tool-based approach to the construction of software artifacts that are supported by rigorous evidence. The DesCert workflow integrates evidence generation into a design process that goes from requirements capture and analysis to the decomposition of the high-level software requirements into architecture properties and software components with assertional contracts, and on to software that can be analyzed both dynamically and statically. The generated evidence is organized by means of an assurance ontology and integrated into the RACK knowledge base., Comment: 142 pages, 63 figures

We present LT-PDR, a lattice-theoretic generalization of Bradley's property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious combination of verification and refutation attempts based on the Knaster-Tarski and Kleene theorems. We introduce four concrete instances of LT-PDR, derive their implementation from a generic Haskell implementation of LT-PDR, and experimentally evaluate them. We also present a categorical structural theory that derives these instances., Comment: 37 pages

In the future, most companies will be confronted with the topic of Artificial Intelligence (AI) and will have to decide on their strategy in this regards. Currently, a lot of companies are thinking about whether and how AI and the usage of data will impact their business model and what potential use cases could look like. One of the biggest challenges lies in coming up with innovative solution ideas with a clear business value. This requires business competencies on the one hand and technical competencies in AI and data analytics on the other hand. In this article, we present the concept of AI innovation labs and demonstrate a comprehensive framework, from coming up with the right ideas to incrementally implementing and evaluating them regarding their business value and their feasibility based on a company's capabilities. The concept is the result of nine years of working on data-driven innovations with companies from various domains. Furthermore, we share some lessons learned from its practical applications. Even though a lot of technical publications can be found in the literature regarding the development of AI models and many consultancy companies provide corresponding services for building AI innovations, we found very few publications sharing details about what an end-to-end framework could look like.

Automated Market Makers (AMMs) are decentralized applications that allow users to exchange crypto-tokens without the need for a matching exchange order. AMMs are one of the most successful DeFi use cases: indeed, major AMM platforms process a daily volume of transactions worth USD billions. Despite their popularity, AMMs are well-known to suffer from transaction-ordering issues: adversaries can influence the ordering of user transactions, and possibly front-run them with their own, to extract value from AMMs, to the detriment of users. We devise an effective procedure to construct a strategy through which an adversary can maximize the value extracted from user transactions., Comment: FC'22 proceedings version with proofs in appendix

This paper outlines two approaches|based on counterexample-guided abstraction refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS), respectively to the automated synthesis of finite-state probabilistic models and programs. Our CEGAR approach iteratively partitions the design space starting from an abstraction of this space and refines this by a light-weight analysis of verification results. The CEGIS technique exploits critical subsystems as counterexamples to prune all programs behaving incorrectly on that input. We show the applicability of these synthesis techniques to sketching of probabilistic programs, controller synthesis of POMDPs, and software product lines., Comment: 18 pages

Vision systems, i.e., systems that allow to detect and track objects in images, have gained substantial importance over the past decades. They are used in quality assurance applications, e.g., for finding surface defects in products during manufacturing, surveillance, but also automated driving, requiring reliable behavior. Interestingly, there is only little work on quality assurance and especially testing of vision systems in general. In this paper, we contribute to the area of testing vision software, and present a framework for the automated generation of tests for systems based on vision and image recognition. The framework makes use of existing libraries allowing to modify original images and to obtain similarities between the original and modified images. We show how such a framework can be used for testing a particular industrial application on identifying defects on riblet surfaces and present preliminary results from the image classification domain., Comment: 4 pages, Submission version, Accepted at the 2nd ACM/IEEE International Conference on Automation of Software Test AST 2021

Capturing users' engagement is crucial for gathering feedback about the features of a software product. In a market-driven context, current approaches to collect and analyze users' feedback are based on techniques leveraging information extracted from product reviews and social media. These approaches are hardly applicable in bespoke software development, or in contexts in which one needs to gather information from specific users. In such cases, companies need to resort to face-to-face interviews to get feedback on their products. In this paper, we propose to utilize biometric data, in terms of physiological and voice features, to complement interviews with information about the engagement of the user on the discussed product-relevant topics. We evaluate our approach by interviewing users while gathering their physiological data (i.e., biofeedback) using an Empatica E4 wristband, and capturing their voice through the default audio-recorder of a common laptop. Our results show that we can predict users' engagement by training supervised machine learning algorithms on biometric data (F1=0.72), and that voice features alone are sufficiently effective (F1=0.71). Our work contributes with one the first studies in requirements engineering in which biometrics are used to identify emotions. This is also the first study in software engineering that considers voice analysis. The usage of voice features could be particularly helpful for emotion-aware requirements elicitation in remote communication, either performed by human analysts or voice-based chatbots, and can also be exploited to support the analysis of meetings in software engineering research., Comment: This paper contains updated experimental results with respect to the initial version

The self-* properties commonly associated with the concept of autonomic computing are capabilities desirable for avionics software platforms. They decrease the configuration effort and inherently provide new fault tolerance and resource savings possibilities. The rigid certification process and the requirements for a static and predetermined system behavior are, however, in contradiction with the adaptive and flexible nature of autonomic computing systems. We propose a partition-based architecture providing autonomic features for avionics software platforms while being compliant to regulations and accepted technologies, such as ARINC 653. The core is a platform consciousness based on a domain-specific model and a novel MAP-QE-K cycle. Moreover, we suggest a planning intelligence, a virtual qualification authority, and a minimized execution unit. For each component we define the required design assurance level and possible realization techniques. We discuss the overall feasibility and point out central challenges in the fields of runtime verification and models at runtime. These challenges need to be solved up to the realization of autonomic avionics, e.g. a virtual security assessment and a qualifiable domain-specific model database., Comment: 7 pages, 5 figures

Context: Conflicts between software requirements bring uncertainties to product development. Some great approaches have been proposed to identify these conflicts. However, they usually require the software requirements represented with specific templates and/or depend on other external source which is often uneasy to build for lots of projects in practice. Objective: We aim to propose an approach Finer Semantic Analysis-based Requirements Conflict Detector (FSARC) to automatically detecting the conflicts between the given natural language functional requirements by analyzing their finer semantic compositions. Method: We build a harmonized semantic meta-model of functional requirements with the form of eight-tuple. Then we propose algorithms to automatically analyze the linguistic features of requirements and to annotate the semantic elements for their semantic model construction. And we define seven types of conflicts as long as their heuristic detecting rules on the ground of their text pattern and semantical dependency. Finally, we design and implement the algorithm for conflicts detection. Results: The experiment with four requirement datasets illustrates that the recall of FSARC is nearly 100% and the average precision is 83.88% on conflicts detection. Conclusion: We provide a useful tool for detecting the conflicts between natural language functional requirements to improve the quality of the final requirements set. Besides, our approach is capable of transforming the natural language functional requirements into eight semantic tuples, which is useful not only the detection of the conflicts between requirements but also some other tasks such as constructing the association between requirements and so on., Comment: 17 pages, 2 figures

Automated market makers (AMMs) are one of the most prominent decentralized finance (DeFi) applications. AMMs allow users to trade different types of crypto-tokens, without the need to find a counter-party. There are several implementations and models for AMMs, featuring a variety of sophisticated economic mechanisms. We present a theory of AMMs. The core of our theory is an abstract operational model of the interactions between users and AMMs, which can be concretised by instantiating the economic mechanisms. We exploit our theory to formally prove a set of fundamental properties of AMMs, characterizing both structural and economic aspects. We do this by abstracting from the actual economic mechanisms used in implementations, and identifying sufficient conditions which ensure the relevant properties. Notably, we devise a general solution to the arbitrage problem, the main game-theoretic foundation behind the economic mechanisms of AMMs.

Lending pools are decentralized applications which allow mutually untrusted users to lend and borrow crypto-assets. These applications feature complex, highly parametric incentive mechanisms to equilibrate the loan market. This complexity makes the behaviour of lending pools difficult to understand and to predict: indeed, ineffective incentives and attacks could potentially lead to emergent unwanted behaviours. Reasoning about lending pools is made even harder by the lack of executable models of their behaviour: to precisely understand how users interact with lending pools, eventually one has to inspect their implementations, where the incentive mechanisms are intertwined with low-level implementation details. Further, the variety of existing implementations makes it difficult to distill the common aspects of lending pools. We systematize the existing knowledge about lending pools, leveraging a new formal model of interactions with users, which reflects the archetypal features of mainstream implementations. This enables us to prove some general properties of lending pools, such as the correct handling of funds, and to precisely describe vulnerabilities and attacks. We also discuss the role of lending pools in the broader context of decentralized finance., Comment: 20 pages. Under submission

The identification of primal variables and adjoint variables is usually done via indices in operator overloading algorithmic differentiation tools. One approach is a linear management scheme, which is easy to implement and supports memory optimization for copy statements. An alternative approach performs a reuse of indices, which requires more implementation effort but results in much smaller adjoint vectors. Therefore, the vector mode of algorithmic differentiation scales better with the reuse management scheme. In this paper, we present a novel approach that reuses the indices and allows the copy optimization, thus combining the advantages of the two aforementioned schemes. The new approach is compared to the known approaches on a simple synthetic test case and a real-world example using the computational fluid dynamics solver SU2., Comment: 15 pages, 4 figures, 4 tables

Various software features such as classes, methods, requirements, and tests often have similar functionality. This can lead to emergence of duplicates in their descriptive documentation. Uncontrolled duplicates created via copy/paste hinder the process of documentation maintenance. Therefore, the task of duplicate detection in software documentation is of importance. Solving it makes planned reuse possible, as well as creating and using templates for unification and automatic generation of documentation. In this paper, we present an interactive process for duplicate detection that involves the user in order to conduct meaningful search. It includes a new formal definition of a near duplicate, a pattern-based, and the proof of its completeness. Moreover, we demonstrate the results of experimenting on a collection of documents of several industrial projects.

Denotational models should provide an opportunity for the revision of current practices seen in the manuals of programming languages. New styles should on one hand base on denotational models but on the other - do not assume that today readers are acquainted in this field. A manual should, therefore, provide some basic knowledge and notation needed to understand the definition of a programming language written in a new style. At the same time - I strongly believe that - it should be written for professional programmers rather than for amateurs. The role of a manual is not to teach the skills of programming. Such textbooks are, of course, necessary, but they should tell the readers what the programming is about rather than the technicalities of a concrete language. The paper contains an example of a manual for a virtual programming language Lingua developed in our project., Comment: 47 pages. This paper is based on my preprinted book 'A Denotational Engineering of Programming Languages' (available on arXiv:1905.01473), which describes a virtual programming language whose manual is discussed in the paper. To make the paper possibly self-contained large parts of the book are quoted in the paper. arXiv admin note: substantial text overlap with arXiv:1905.01469

Software testing is an important issue in software development process to ensure higher quality on the products. Formal methods has been promising on testing reactive systems, specially critical systems, where accuracy is mandatory since any fault can cause severe damage. Systems of this nature are characterized by receiving messages from the environment and producing outputs in response. One of the most challenges in model-based testing is the conformance checking of asynchronous reactive systems. The aim is to verify if an implementation is in compliance with its respective specification. In this work, we develop a practical tool to check conformance relation between reactive models using a more general theory based on regular languages. The approach, in fact, subsumes the classical \ioco conformance which is also available in our tool. In addition, we present some studies with different sceneries that are applied to practical tools with both notions of conformance., Comment: 18 pages, 9 figures, 5 algorithms

The paper is devoted to showing how to systematically design a programming language in 'reverse order', i.e. from denotations to syntax. This construction is developed in an algebraic framework consisting of three many-sorted algebras: of denotations, of an abstract syntax and of a concrete syntax. These algebras are constructed in such a way that there is a unique homomorphism from concrete syntax to denotations, which constitutes the denotational semantics of the language. Besides its algebraic framework, the model is set-theoretic, i.e. the denotational domains are just sets, rather than Scott's reflexive domains. The method is illustrated by a layer-by-layer development of a virtual language Lingua: an applicative layer, an imperative layer (with recursive procedures) and an SQL layer where Lingua is regarded as an API (Application Programming Interface) for an SQL engine. The latter is given a denotational semantics as well. The langue is equipped with a strong typing mechanism which covers basic types (numbers, Booleans, etc.), lists, arrays, record and their arbitrary combinations plus SQL-like types: rows, tables and databases. The model of types includes SQL integrity constraints., Comment: A preprint of 44 pages. All comments will be highly appreciated. You may contact me on andrzej.blikle@moznainaczej.com.pl

The book is devoted to two research areas: (1) Designing programming languages along with their denotational models. A denotational model of a language consists of two many-sorted algebras - an algebra of syntax and an algebra of denotations - and a (unique) homomorphism from syntax to denotations called the semantics of the language. (2) Designing sound program-constructors for languages with denotational models. In our approach programs syntactically contain their total-correctness specifications. A program is said to be correct if it is correct wrt its specification. A program-constructor is sound if given correct component-programs yields a correct resulting program. Both methods are illustrated on an example-language Lingua., Comment: A preprint of a book; 340 pages. All comments will be highly appreciated. You may write to me on andrzej.blikle@moznainaczej.com.pl

Verification of programs using floating-point arithmetic is challenging on several accounts. One of the difficulties of reasoning about such programs is due to the peculiarities of floating-point arithmetic: rounding errors, infinities, non-numeric objects (NaNs), signed zeroes, denormal numbers, different rounding modes, etc. One possibility to reason about floating-point arithmetic is to model a program computation path by means of a set of ternary constraints of the form z = x op y and use constraint propagation techniques to infer new information on the variables' possible values. In this setting, we define and prove the correctness of algorithms to precisely bound the value of one of the variables x, y or z, starting from the bounds known for the other two. We do this for each of the operations and for each rounding mode defined by the IEEE 754 binary floating-point standard, even in the case the rounding mode in effect is only partially known. This is the first time that such so-called filtering algorithms are defined and their correctness is formally proved. This is an important slab for paving the way to formal verification of programs that use floating-point arithmetics., Comment: 64 pages, 19 figures, 2 tables

We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochastic disturbances. Our method derives digital controllers such that the corresponding closed-loop system, modeled as a sampled-data stochastic control system, satisfies a safety specification with probability above a given threshold. The proposed synthesis method alternates between two steps: generation of a candidate controller pc, and verification of the candidate. pc is found by maximizing a Monte Carlo estimate of the safety probability, and by using a non-validated ODE solver for simulating the system. Such a candidate is therefore sub-optimal but can be generated very rapidly. To rule out unstable candidate controllers, we prove and utilize Lyapunov's indirect method for instability of sampled-data nonlinear systems. In the subsequent verification step, we use a validated solver based on SMT (Satisfiability Modulo Theories) to compute a numerically and statistically valid confidence interval for the safety probability of pc. If the probability so obtained is not above the threshold, we expand the search space for candidates by increasing the controller degree. We evaluate our technique on three case studies: an artificial pancreas model, a powertrain control model, and a quadruple-tank process., Comment: 12 pages, 4 figures, 4 tables

Numerical software are widely used in safety-critical systems such as aircrafts, satellites, car engines and so on, facilitating dynamics control of such systems in real time, it is therefore absolutely necessary to verify their correctness. It is a long standing challenge to guarantee verified properties of numerical software are indeed satisfied by their real behaviours, because most of these verifications are conducted under ideal mathematical models, but their real executions could be influenced essentially by uncertain inputs accounting for round-off errors and additive perturbations from real-world phenomena to hardware, which are abstracted away in these ideal mathematical models. In this paper, we attempt to address this issue focusing on nontermination analysis of numerical software, where nontermination is often an unexpected behaviour of computer programs and may be problematic for applications such as real-time systems having hard deadlines on transaction execution time, and propose a method for robust conditional nontermination analysis, which can be used to under-approximate the maximal robust nontermination input set for a given program, from which the program never terminates, regardless of the aforementioned disturbances. Finally, several examples are employed to illustrate our approach., Comment: 10 pages, five figures

DCSYNTH is a tool for the synthesis of controllers from safety and bounded liveness requirements given in interval temporal logic QDDC. It investigates the role of soft requirements (with priorities) in obtaining high quality controllers. A QDDC formula specifies past time properties. In DCSYNTH synthesis, hard requirements must be invariantly satisfied whereas soft requirements may be satisfied "as much as possible" in a best effort manner by the controller. Soft requirements provide an invaluable ability to guide the controller synthesis. In the paper, using DCSYNTH, we show the application of soft requirements in obtaining robust controllers with various specifiable notions of robustness. We also show the use of soft requirements to specify and synthesize efficient runtime enforcement shields which can correct burst errors. Finally, we discuss the use of soft requirements in improving the latency of controlled system.

The important feature of temporal model checking is the generation of counterexamples. In the report, the requirements for generation of counterexample (called critical tree) in model checking of CSM systems are described. The output of TempoRG model checker for QsCTL logic (a version of CTL) is presented. A contradiction between counterexample generation and state space reduction is commented., Comment: 20 pages, 12 figures

During the project of a communication protocol, many design decisions influence the behavior of the protocol and its correctness. Formal specification and verification of the protocol may prove its correctness. In this paper, an example of a verification of design decision using formal specification in CSM automata and verification in temporal logic is presented., Comment: 15 pages, 7 figures

Classical CTL temporal logics are built over systems with interleaving model concurrency. Many attempts are made to fight a state space explosion problem (for instance, compositional model checking). There are some methods of reduction of a state space based on independence of actions. However, in CSM model, which is based on coincidences rather than on interleaving, independence of actions cannot be defined. Therefore a state space reduction basing on identical temporal consequences rather than on independence of action is proposed. The new reduction is not as good as for interleaving systems, because all successors of a state (in depth of two levels) must be obtained before a reduction may be applied. This leads to reduction of space required for representation of a state space, but not in time of state space construction. Yet much savings may occur in regular state spaces for CSM systems., Comment: 12 pages, 10 figures

In ICS, WUT a COSMA design environment is being developed. COSMA is based on Concurrent State Machines (CSM) formalism of system specification. It contains a graphical tool for system design, various tools for the analysis (including a temporal model checker), simulator and code generator. In many projects, some common susbsystems take place. This concerns both complicated modules and simple counters. In the report, a concept of macrogeneration technique for building of libraries of automata is presented. The new technique will support a compactness of projects and reusability of modules., Comment: 26 pages, 14 figures

There are several AD tools available, which all implement different strategies for the reverse mode of AD. The major strategies are primal value taping (implemented e.g. by ADOL-c) and Jacobi taping (implemented e.g. by adept and dco/c++). Especially for Jacobi taping, recent advances by using expression templates make this approach very attractive for large scale software. The current implementations are either closed source or miss essential features and flexibility. Therefore, we present the new AD tool CoDiPack (Code Differentiation Package) in this paper. It is specifically designed for a minimal memory consumption and optimal runtime, such that it can be used for the differentiation of large scale software. An essential part of the design of CoDiPack is the modular layout and the recursive data structures, which do not only allow the efficient implementation of the Jacobi taping approach, but will also enable other approaches like the primal value taping or new research ideas. We will also present the performance value of CoDiPack on a generic PDE example and on the SU2 code., Comment: 21 pages, 11 figures, 6 tables, CoDiPack: https://github.com/SciCompKL/CoDiPack

Self-adaptive software is considered as the most advanced approach and its development attracts a lot of attention. Decentralization is an effective way to design and manage the complexity of modern self-adaptive software systems. However, there are still tremendous challenges. One major challenge is to unify decentrality with traditional self-adaptive implementation framework during design and implementation activity. One is to guarantee the required global goals and performance of decentralized self-adaptive systems operating in highly dynamic and uncertain environments. Another challenge is to predict the influence of system's internal change on its self-adaptability to the environment. To solve these problems, we combine the mechanisms of separation of concerns with modeling method using timed automata to allow the system to be analyzed and verified. Timed computation tree logic is used to specify system goals and stochastic simulations in dynamic environment are experimented to verify decentralized self-adaptive system's adaptation properties. In this paper, we extracted a motivation example from practical applications in UAV emergency mission scenarios. The whole approach is evaluated and illustrated with this motivation example and the statistical results can be used as reference for arrangement planning of UAVs in cyber physical spaces., Comment: The hypotheses at the beginning of the article are wrong. There are also errors in the paper, especially in the experiments section

Several temporal logics have been proposed to formalise timing diagram requirements over hardware and embedded controllers. These include LTL, discrete time MTL and the recent industry standard PSL. However, succintness and visual structure of a timing diagram are not adequately captured by their formulae. Interval temporal logic QDDC is a highly succint and visual notation for specifying patterns of behaviours. In this paper, we propose a practically useful notation called SeCeCntnl which enhances negation free fragment of QDDC with features of nominals and limited liveness. We show that timing diagrams can be naturally (compositionally) and succintly formalized in SeCeCntnl as compared with PSL and MTL. We give a linear time translation from timing diagrams to SeCeCntnl. As our second main result, we propose a linear time translation of SeCeCntnl into QDDC. This allows QDDC tools such as DCVALID and DCSynth to be used for checking consistency of timing diagram requirements as well as for automatic synthesis of property monitors and controllers. We give examples of a minepump controller and a bus arbiter to illustrate our tools. Giving a theoretical analysis, we show that for the proposed SeCeCntnl, the satisfiability and model checking have elementary complexity as compared to the non-elementary complexity for the full logic QDDC.

An engineering design process may involve software modules that can executed concurrently. Concurrent modules can be very easily subject to some synchronization errors. This paper discusses verification process for such engineering software. We present a method for verification that requires several steps. First, the state diagram models are constructed that describe the design iterations and interactions with the designer. Next, the state diagram models are transformed into concurrent state machines (CSM). After that, the CSM models are analyzed in order to verify their correctness. In this phase, the modifications are performed in necessary. In the last phase the code is generated. The tools to support our method can be called new concurrent CASE tools. Using these tools the engineering software can be created that is verified for correctness in respect to concurrent execution., Comment: 9 pages, 12 figures

Self-adaptive software (SAS) is capable of adjusting its behavior in response to meaningful changes in the operational context and itself. Due to the inherent volatility of the open and changeable environment in which SAS is embedded, the ability of adaptation is highly demanded by many software-intensive systems. Two concerns, i.e., the requirements uncertainty and the context uncertainty are most important among others at Requirements Engineering (RE) stage. However, requirements analyzers can hardly figure out the mathematical relation between requirements, system behavior and context, especially for complex and nonlinear systems, due to the existence of above uncertainties, misunderstanding and ambiguity of prior knowledge. An essential issue to be addressed is how to model and specify these uncertainties at RE stage and how to utilize the prior knowledge to achieve adaptation. In this paper, we propose a fuzzy-based approach to modeling uncertainty and achieving evolution. The approach introduces specifications to describe fuzziness. Based on the specifications, we derive a series of reasoning rules as knowledge base for achieving adaptation and evolution. These two targets are implemented through four reasoning schemas from a control theory perspective. Specifically, forward reasoning schema is used for direct adaptation; backward reasoning schema is used for optimal adaptation. Parameter-identified schema implements learning evolution by considering SAS as the gray-box system, while system-identified reasoning schema implements learning evolution by considering SAS as the gray-box system. The former two schemas function as the control group, while the latter two are de-signed as the experimental groups to illustrate the learning ability. Our approach is implemented under three types of context through the demonstration of a mobile computing application., Comment: The CHN extension of this article has been accepted bu Journal of Computer Research and Development. Keywords: self-adaptive software, requirements engineering, uncertainty, evolution, fuzzy theory, control theory