Endre søk
Begrens søket
12 1 - 50 of 64
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Treff pr side
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
  • Standard (Relevans)
  • Forfatter A-Ø
  • Forfatter Ø-A
  • Tittel A-Ø
  • Tittel Ø-A
  • Type publikasjon A-Ø
  • Type publikasjon Ø-A
  • Eldste først
  • Nyeste først
  • Skapad (Eldste først)
  • Skapad (Nyeste først)
  • Senast uppdaterad (Eldste først)
  • Senast uppdaterad (Nyeste først)
  • Disputationsdatum (tidligste først)
  • Disputationsdatum (siste først)
Merk
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1.
    Ahrendt, Wolfgang
    et al.
    Chalmers University of Technology, Gothenburg, Sweden.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Johansson, Moa
    Chalmers University of Technology, Gothenburg, Sweden.
    Rümmer, Philipp
    University of Regensburg, Regensburg, Germany; Uppsala University, Uppsala, Sweden.
    TriCo—Triple Co-piloting of Implementation, Specification and Tests2022Inngår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature , 2022, Vol. 13701 LNCS, s. 174-187Konferansepaper (Fagfellevurdert)
    Abstract [en]

    This white paper presents the vision of a novel methodology for developing safety-critical software, which is inspired by late developments in learning based co-piloting of implementations. The methodology, called TriCo, integrates formal methods with learning based approaches to co-pilot the agile, simultaneous development of three artefacts: implementation, specification, and tests. Whenever the user changes any of these, a TriCo empowered IDE would suggest changes to the other two artefacts in such a way that the three are kept consistent. The user has the final word on whether the changes are accepted, rejected, or modified. In the latter case, consistency will be checked again and re-established. We discuss the emerging trends which put the community in a good position to realise this vision, describe the methodology and workflow, as well as challenges and possible solutions for the realisation of TriCo.

  • 2.
    Aktug, Irem
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS. KTH, Skolan för elektro- och systemteknik (EES), Centra, ACCESS Linnaeus Centre.
    Dam, Mads
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS. KTH, Skolan för elektro- och systemteknik (EES), Centra, ACCESS Linnaeus Centre.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Provably Correct Runtime Monitoring2009Inngår i: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 78, nr 5, s. 304-339Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    Runtime monitoring is an established technique to enforce a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has a copy of the given monitor embedded into it. As the main application of these results we sketch a simple inlining algorithm and show how the two-level annotations can be completed to produce a fully annotated program which is valid in the standard sense of Floyd/Hoare logic. This establishes the mediation property that inlined programs are guaranteed to adhere to the intended policy. Furthermore, validity can be checked efficiently using a weakest precondition based annotation checker, thus preparing the ground for on-device checking of policy adherence in a proof-carrying code setting.

  • 3.
    Aktug, Irem
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Dam, Mads
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Provably correct runtime monitoring (extended abstract)2008Inngår i: Fm 2008: Formal Methods, Proceedings / [ed] Cuellar, J; Maibaum, T; Sere, K, 2008, Vol. 5014, s. 262-277Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Runtime monitoring is an established technique for enforcing a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has an instance of the given monitor embedded into it, which yields state changes at prescribed points according to the monitor's transition function. As our main application of these results we describe a concrete inliner, and use the annotation scheme to characterize its correctness. For this inliner, correctness of the level II annotations can be decided efficiently by a weakest precondition annotation checker, thus allowing on-device checking of inlining correctness in a proof-carrying code setting.

  • 4.
    Aktug, Irem
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Numerisk Analys och Datalogi, NADA.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Numerisk Analys och Datalogi, NADA.
    State Space Representation for Verification of Open Systems2006Inngår i: Algebraic Methodology And Software Technology, Proceedings / [ed] Johnson, M; Vene, V, Berlin: Springer , 2006, s. 5-20Konferansepaper (Fagfellevurdert)
    Abstract [en]

    When designing an open system, there might be no implementation available for certain components at verification time. For such systems, verification has to be based on assumptions on the underspecified components. When component assumptions are expressed in Hennessy-Milner logic (HML), the state space of open systems can be naturally represented with modal transition systems (NITS), a graphical specification language equiexpressive with HML. Having an explicit state space representation supports state space exploration based verification techniques, Besides, it enables proof reuse and facilitates visualization for the user guiding the verification process. in interactive verification. As an intuitive representation of system behavior, it aids debugging when proof generation fails in automatic verification.

    However, HML is not expressive enough to capture temporal assumptions. For this purpose, we extend MTSs to represent the state space of open systems where component assumptions are specified in modal mu-calculus. We present a two-phase construction from process algebraic open system descriptions to such state space representations. The first phase deals with component assumptions, and is essentially a maximal model construction for the modal p-calculus. In the second phase, the models obtained are combined according to the structure of the open system to form the complete state space. The construction is sound and complete for systems with a single unknown component and sound for those-without dynamic process creation. For establishing open system properties based on the representation, we present a proof system which is sound and complete for prime formulae.

  • 5.
    Aktug, Irem
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Towards State Space Exploration Based Verification of Open Systems2005Inngår i: 4th International Workshop on Automated Verification of Infinite-State Systems (AVIS’05), April 2005, Edinburgh, Scotland, 2005Konferansepaper (Fagfellevurdert)
  • 6.
    Alshnakat, Anoud
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lidström, Christian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Rümmer, P.
    Constraint-Based Contract Inference for Deductive Verification2020Inngår i: Deductive Software Verification: Future Perspectives, Springer Nature , 2020, s. 149-176Kapittel i bok, del av antologi (Fagfellevurdert)
    Abstract [en]

    Assertion-based software model checking refers to techniques that take a program annotated with logical assertions and statically verify that the assertions hold whenever program execution is at the corresponding control point. While the associated annotation overhead is relatively low, these techniques are typically monolithic in that they explore the state space of the whole program at once, and may therefore scale poorly to large programs. Deductive software verification, on the other hand, refers to techniques that prove the correctness of a piece of software against a detailed specification of what it is supposed to accomplish or compute. The associated verification techniques are modular and scale well to large code bases, but incur an annotation overhead that is often very high, which is a real obstacle for deductive verification to be adopted in industry on a wider scale. In this paper we explore synergies between the two mentioned paradigms, and in particular, investigate how interpolation-based Horn solvers used for software model checking can be instrumented to infer missing procedure contracts for use in deductive verification, thus aiding the programmer in the code annotation process. We summarise the main developments in the area of automated contract inference, and present our own experiments with contract inference for C programs, based on solving Horn clauses. To drive the inference process, we put program assertions in the main function, and adapt our TriCera tool, a model checker based on the Horn solver Eldarica, to infer candidate contracts for all other functions. The contracts are output in the ANSI C Specification Language (ACSL) format, and are then validated with the Frama-C deductive verification tool for C programs.

  • 7.
    Amighi, Afshin
    et al.
    University of Twente.
    de Carvalho Gomes, Pedro
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, Marieke
    University of Twente.
    Provably Correct Control Flow Graphs from Java Bytecode Programs with Exceptions2016Inngår i: International Journal on Software Tools for Technology Transfer, ISSN 1433-2779, E-ISSN 1433-2787, ISSN 1433-2779, Vol. 18, nr 6, s. 653-684Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present an algorithm for extracting control flow graphs from Java bytecode that captures normal as well as exceptional control flow. We prove its correctness, in the sense that the behaviour of the extracted control flow graph is a sound over-approximation of the behaviour of the original program. This makes control flow graphs suitable for performing various static analyses, such as model checking of temporal safety properties.Analyzing exceptional control flow for Java bytecode is difficult because of the stack-based nature of the language. We therefore develop the extraction in two stages. In the first, we abstract away from the complications arising from exceptional flows, and relativize the extraction on an oracle that is able to look into the stack and predict the exceptions that can be raised at each instruction. This idealized algorithm provides a specification for concrete extraction algorithms, which have to provide a suitable implementation for the oracle. We prove correctness of the idealized algorithm by means of behavioural simulation.In the second stage, we develop a concrete extraction algorithm that consists of two phases. In the first phase, the program is transformed into a BIR program, a stack-less intermediate representation of Java bytecode, from which the control flow graph is extracted in the second phase. We use this intermediate format because it provides the information needed to implement the oracle, and since it gives rise to more compact graphs. We show that the behaviour of the control flow graph extracted via the intermediate representation is a sound over-approximation of the behaviour of the graph extracted by the direct, idealized algorithm, and thus of the original program. The concrete extraction algorithm is implemented as the ConFlEx tool. A number of test cases are performed to evaluate the efficiency of the algorithm.

  • 8.
    Amighi, Afshin
    et al.
    University of Twente.
    de Carvalho Gomes, Pedro
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, Marieke
    University of Twente.
    Provably Correct Control-Flow Graphs from Java Programs with Exceptions2012Rapport (Annet vitenskapelig)
    Abstract [en]

    We present an algorithm to extract flow graphs from Java bytecode, including exceptional control flows. We prove its correctness, meaning that the behavior of the extracted control-flow graph is a sound over-approximation of the behavior of the original program. Thus any safety property that holds for the extracted control-flow graph also holds for the original program. This makes control-flow graphs suitable for performing various static analyses, such as model checking.The extraction is performed in two phases. In the first phase the program is transformed into a BIR program, a stack-less intermediate representation of Java bytecode, from which the control-flow graph is extracted in the second phase. We use this intermediate format because it results in compact flow graphs, with provably correct exceptional control flow. To prove the correctness of the two-phase extraction, we also define an idealized extraction algorithm, whose correctness can be proven directly. Then we show that the behavior of the control-flow graph extracted via the intermediate representation is an over-approximation of the behavior of the directly extracted graphs, and thus of the original program. We implemented the indirect extraction as the CFGEx tool and performed several test-cases to show the efficiency of the algorithm.

    Fulltekst (pdf)
    fulltext
  • 9.
    Amighi, Afshin
    et al.
    University of Twente.
    de Carvalho Gomes, Pedro
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, Marieke
    University of Twente.
    Sound Control-Flow Graph Extraction for Java Programs with Exceptions2012Inngår i: Software Engineering and Formal Methods: 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings, Springer Berlin/Heidelberg, 2012, s. 33-47Konferansepaper (Fagfellevurdert)
    Abstract [en]

    We present an algorithm to extract control-flow graphs from Java bytecode, considering exceptional flows. We then establish its correctness: the behavior of the extracted graphs is shown to be a sound over-approximation of the behavior of the original programs. Thus, any temporal safety property that holds for the extracted control-flow graph also holds for the original program. This makes the extracted graphs suitable for performing various static analyses, in particular model checking. The extraction proceeds in two phases. First, we translate Java bytecode into BIR, a stack-less intermediate representation. The BIR transformation is developed as a module of Sawja, a novel static analysis framework for Java bytecode. Besides Sawja’s efficiency, the resulting intermediate representation is more compact than the original bytecode and provides an explicit representation of exceptions. These features make BIR a natural starting point for sound control-flow graph extraction. Next, we formally define the transformation from BIR to control-flow graphs, which (among other features) considers the propagation of uncaught exceptions within method calls. We prove the correctness of the two-phase extraction by suitably combining the properties of the two transformations with those of an idealized control-flow graph extraction algorithm, whose correctness has been proved directly. The control-flow graph extraction algorithm is implemented in the ConFlEx tool. A number of test-cases show the efficiency and the utility of the implementation.

  • 10.
    Amilon, Jesper
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Esen, Zafer
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lidström, Christian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Rümmer, Philipp
    An Exercise in Mind Reading: Automatic Contract Inference for Frama-C2024Inngår i: Guide to Software Verification with Frama-C: Core Components, Usages, and Applications, Springer Nature, 2024Kapittel i bok, del av antologi (Annet vitenskapelig)
  • 11.
    Amilon, Jesper
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Esen, Zafer
    Uppsala University, Uppsala, Sweden.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lidström, Christian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Rümmer, Philipp
    Uppsala University, Uppsala, Sweden; University of Regensburg, Regensburg, Germany.
    Automatic Program Instrumentation for Automatic Verification2023Inngår i: Computer Aided Verification: 35th International Conference, CAV 2023, Proceedings, Springer Nature , 2023, s. 281-304Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.

  • 12.
    Amilon, Jesper
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lidström, Christian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Deductive Verification Based Abstraction for Software Model Checking2022Inngår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature , 2022, Vol. 13701 LNCS, s. 7-28Konferansepaper (Fagfellevurdert)
    Abstract [en]

    The research community working on formal software verification has historically evolved into two main camps, grouped around two verification methods that are typically referred to as Deductive Verification and Model Checking. In this paper, we present an approach that applies deductive verification to formally justify abstract models for model checking in the TLA framework. We present a proof-of-concept tool chain for C programs, based on Frama-C for deductive verification and TLA+ for model checking. As a theoretical foundation, we summarise a previously developed abstract contract theory as a framework for combining these two methods. Since the contract theory adheres to the principles of contract based design, this justifies the use of the approach in a real-world system design setting. We evaluate our approach on two case studies: a simple C program simulating opening and closing of files, as well as a C program based on real software from the automotive industry.

  • 13.
    Bakhshi, Rana
    et al.
    KTH, Skolan för informations- och kommunikationsteknik (ICT).
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Verification of Peer-to-peer Algorithms: A Case Study2007Inngår i: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 181, nr 1, s. 35-47Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    The problem of maintaining structured peer-to-peer (P2P) overlay networks in the presence of concurrent joins and failures of nodes is the subject of intensive research. The various algorithms underlying P2P systems are notoriously difficult to design and analyse. Thus, when verifying P2P algorithms, a real challenge is to find an adequate level of abstraction at which to model the algorithms and perform the verifications. In this paper, we propose an abstract model for structured P2P networks with ring topology. Our model is based on process algebra, which, with its well-developed theory, provides the right level of abstraction for the verification of many basic P2P algorithms. As a case study, we verify the correctness of the stabilization algorithm of Chord, one of the best-known P2P overlay networks. To show the correctness of the algorithm, we provide a specification and an implementation of the Chord system in process algebra and establish bisimulation equivalence between the two.

  • 14. Borgström, Johannes
    et al.
    Nestmann, Uwe
    Onana, Luc Alima
    KTH, Skolan för informations- och kommunikationsteknik (ICT), Mikroelektronik och Informationsteknik, IMIT.
    Gurov, Dilian
    KTH, Skolan för informations- och kommunikationsteknik (ICT), Mikroelektronik och Informationsteknik, IMIT.
    Verifying a structured peer-to-peer overlay network: The static case2005Inngår i: GLOBAL COMPUTING, 2005, Vol. 3267, s. 250-265Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Structured peer-to-peer overlay networks are a class of algorithms that provide efficient message routing for distributed applications using a sparsely connected communication network. In this paper, we formally verify a typical application running on a fixed set of nodes. This work is the foundation for studies of a more dynamic system. We identify a value and expression language for a value-passing CCS that allows us to formally model a distributed hash table implemented over a static DKS overlay network. We then provide a specification of the lookup operation in the same language, allowing us to formally verify the correctness of the system in terms of observational equivalence between implementation and specification. For the proof, we employ an abstract notation for reachable states that allows us to work conveniently up to structural congruence, thus drastically reducing the number and shape of states to consider. The structure and techniques of the correctness proof are reusable for other overlay networks.

  • 15.
    Bubel, Richard
    et al.
    Technical University of Darmstadt, Darmstadt, Germany.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Hahnle, Reiner
    Technical University of Darmstadt, Darmstadt, Germany.
    Scaletta, Marco
    Technical University of Darmstadt, Darmstadt, Germany.
    Trace-based Deductive Verification2023Inngår i: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair , 2023, Vol. 94, s. 73-95Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Contracts specifying a procedure’s behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction. We propose a logic over symbolic traces able to specify recursive procedures in a modular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics. Our work generalizes contract-based to trace-based deductive verification by extending the notion of state-based contracts to trace-based contracts.

  • 16.
    Dam, Mads
    et al.
    KTH, Tidigare Institutioner (före 2005), Mikroelektronik och informationsteknik, IMIT.
    Gurov, Dilian
    mu-calculus with explicit points and approximations2002Inngår i: Journal of logic and computation (Print), ISSN 0955-792X, E-ISSN 1465-363X, Vol. 12, nr 2, s. 255-269Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a Gentzen-style sequent calculus for program verification which accommodates both model checking-like verification based on global state space exploration, and compositional reasoning. To handle the complexities arising from the presence of fixed-point formulas, programs with dynamically evolving architecture, and cut rules we use transition assertions, and introduce fixed-point approximants explicitly into the assertion language. We address, in a game-based manner, the semantical basis of this approach, as it applies to the entailment subproblem. Soundness and completeness results are obtained, and examples are shown illustrating some of the concepts.

  • 17.
    de C. Gomes, Pedro
    et al.
    KTH.
    Gurov, Dilian
    KTH.
    Huisman, M.
    Artho, Cyrille
    KTH.
    Specification and verification of synchronization with condition variables2018Inngår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 163, s. 174-189Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    This paper proposes a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness of synchronization as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization block”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviours. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behaviour of the program, which is typically significantly smaller than its overall behaviour. First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. We consider a SyncTask program to have a correct synchronization iff it terminates. Further, to relieve the programmer from the burden of providing specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behaviour of the underlying program. We show that every Java program annotated according to the scheme (and satisfying the assumption mentioned above) has a correct synchronization iff its corresponding SyncTask program terminates. We then show how to transform the verification of termination of the SyncTask program into a standard reachability problem over Coloured Petri Nets that is efficiently solvable by existing Petri Net analysis tools. Both the SyncTask program extraction and the generation of Petri Nets are implemented in our STAVE tool. We evaluate the proposed framework on a number of test cases.

  • 18.
    De Carvalho Gomes, Pedro
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, M.
    Specification and verification of synchronization with condition variables2017Inngår i: 5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016, Springer, 2017, Vol. 694, s. 3-19Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In this paper we propose a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviors. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behavior of the program, which is typically significantly smaller than its overall behavior. First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. We consider a SyncTask program to have a correct synchronization iff it terminates. Further, to relieve the programmer from the burden of providing specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behavior of the underlying program. We prove that every Java program annotated according to the scheme (and satisfying the assumption) has a correct synchronization iff its corresponding SyncTask program terminates. We show how to transform the verification of termination into a standard reachability problem over Colored Petri Nets that is efficiently solvable by existing Petri Net analysis tools. Both the SyncTask program extraction and the generation of Petri Nets are implemented in our STaVe tool. We evaluate the proposed framework on a number of test cases as a proof-of-concept.

  • 19.
    de Carvalho Gomes, Pedro
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, Marieke
    University of Twente.
    Algorithmic Verification of Synchronization with Condition Variables2015Rapport (Annet vitenskapelig)
    Abstract [en]

    Condition variables are a common synchronization mechanism present in many programming languages. Still, due to the combinatorial complexity of the behaviours the mechanism induces, it has not been addressed sufficiently with formal techniques. In this paper we propose a fully automated technique to prove the correct synchronization of concurrent programs synchronizing via condition variables, where under correctness we mean the liveness property: "If for every set of condition variables, every thread synchronizing under the variables of the set eventually enters its synchronization block, then every thread will eventually exit the synchronization".First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. Next, we model the constructs of the language as Petri Net components, and define rules to extract and compose nets from a SyncTask program. We show that a SyncTask program terminates if and only if the corresponding Petri Net always reaches a particular final marking. We thus transform the verification of termination into a reachability problem on the net, which can be solved efficiently by existing Petri Net analysis tools. Further, to relieve the programmer from the burden of having to provide specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behaviour of the underlying program. We show that, for the Java programs that can be annotated according to the scheme, the above-mentioned liveness property holds if and only if the corresponding SyncTask program terminates. Both the SyncTask program extraction and the generation of Petri Nets are implemented in the STaVe tool. We evaluate the proposed verification framework on a number of test cases

    Fulltekst (pdf)
    Report
  • 20.
    de Carvalho Gomes, Pedro
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Picoco, Attilio
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS. Polytechnic University of Turin.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Sound Control Flow Graph Extraction from Incomplete Java Bytecode Programs2014Inngår i: Fundamental Approaches to Software Engineering: 17th International Conference, FASE 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings / [ed] Stefania Gnesi and Arend Rensink, Springer Berlin/Heidelberg, 2014, s. 215-229Konferansepaper (Fagfellevurdert)
    Abstract [en]

    The modular analysis of control flow of incompleteJava bytecode programs is challenging, mainly because of the complex semantics of the language,and the unknown inter-dependencies between the available and unavailable components.In this paper we describe a technique for incremental, modular extraction ofcontrol flow graphs that are provably sound w.r.t.~sequences of method invocations and exceptions.The extracted models are suitable for various program analyses,in particular model-checking of temporal control flow safety properties.Soundness comes at the price of over-approximation,potentially giving rise to false positives reports during verification.Still, our technique supports incremental refinement of the already extracted models,as more components code becomes available.The extraction has been implemented as the ConFlex tool, and test-cases show its utility and efficiency.

  • 21.
    de Carvalho Gomes, Pedro
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Picoco, Attilio
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Sound Extraction of Control-Flow Graphs from open Java Bytecode Systems2012Rapport (Annet vitenskapelig)
    Abstract [en]

    Formal verification techniques have been widely deployed as means to ensure the quality of software products. Unfortunately, they suffer with the combinatorial explosion of the state space. That is, programs have a large number of states, sometimes infinite. A common approach to alleviate the problem is to perform the verification over abstract models from the program. Control-flow graphs (CFG) are one of the most common models, and have been widely studied in the past decades. Unfortunately, previous works over modern programming languages, such as Java, have either neglected features that influence the control-flow, or do not provide a correctness argument about the CFG construction. This is an unbearable issue for formal verification, where soundness of CFGs is a mandatory condition for the verification of safety-critical properties. Moreover, one may want to extract CFGs from the available components of an open system. I.e., a system whose at least one of the components is missing. Soundness is even harder to achieve in this scenario, because of the unknown inter-dependences between software components.

    In the current work we present a framework to extract control-flow graphs from open Java Bytecode systems in a modular fashion. Our strategy requires the user to provide interfaces for the missing components. First, we present a formal definition of open Java bytecode systems. Next, we generalize a previous algorithm that performs the extraction of CFGs for closed programs to a modular set-up. The algorithm uses the user-provided interfaces to resolve inter-dependences involving missing components. Eventually the missing components will arrive, and the open system will become closed, and can execute. However, the arrival of a component may affect the soundness of CFGs which have been extracted previously. Thus, we define a refinement relation, which is a set of constraints upon the arrival of components, and prove that the relation guarantees the soundness of CFGs extracted with the modular algorithm. Therefore, the control-flow safety properties verified over the original CFGs still hold in the refined model.

    We implemented the modular extraction framework in the ConFlEx tool. Also, we have implemented the reusage from previous extractions, to enable the incremental extraction of a newly arrived component. Our technique performs substantial over-approximations to achieve soundness. Despite this, our test cases show that ConFlEx is efficient. Also, the extraction of the CFGs gets considerable speed-up by reusing results from previous analyses.

    Fulltekst (pdf)
    fulltext
  • 22.
    Eshghie, Mojtaba
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Artho, Cyrille
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Dynamic Vulnerability Detection on Smart Contracts Using Machine Learning2021Inngår i: Proceedings Of Evaluation And Assessment In Software Engineering (EASE 2021), Association for Computing Machinery (ACM) , 2021, s. 305-312Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In this work we propose Dynamit, a monitoring framework to detect reentrancy vulnerabilities in Ethereum smart contracts. The novelty of our framework is that it relies only on transaction metadata and balance data from the blockchain system; our approach requires no domain knowledge, code instrumentation, or special execution environment. Dynamit extracts features from transaction data and uses a machine learning model to classify transactions as benign or harmful. Therefore, not only can we find the contracts that are vulnerable to reentrancy attacks, but we also get an execution trace that reproduces the attack. Using a random forest classifier, our model achieved more than 90 percent accuracy on 105 transactions, showing the potential of our technique.

  • 23. Felderer, M.
    et al.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Huisman, M.
    Lisper, B.
    Schlick, R.
    Formal methods in industrial practice - Bridging the gap (track summary)2018Inngår i: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018, Springer, 2018, Vol. 11247, s. 77-81Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Already for many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief, and many individual success stories, no real change in industrial software development seems to happen. In fact, the software industry is moving fast forward itself, and the gap between what formal methods can achieve, and the daily software development practice does not seem to get smaller (and might even be growing).

  • 24.
    Filipovikj, Predrag
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS. Scania CV AB, Södertälje, Sweden.
    Ung, G.
    Scania CV AB, Södertälje, Sweden.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Nyberg, Mattias
    KTH, Skolan för industriell teknik och management (ITM), Maskinkonstruktion, Mekatronik och inbyggda styrsystem. Scania CV AB, Södertälje, Sweden.
    Bounded Invariant Checking for Stateflow2022Inngår i: Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association , 2022, s. 38-52Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Stateflow models are complex software models, often used as part of industrial safety-critical software solutions designed with Matlab Simulink. Being part of safety-critical solutions, these models require the application of rigorous verification techniques for assuring their correctness. In this paper, we propose a refutation-based formal verification approach for analyzing Stateflow models against invariant properties, based on bounded model checking (BMC). The crux of our technique is: i) a representation of the state space of Stateflow models as a symbolic transition system (STS) over the symbolic configurations of the model, and ii) application of incremental BMC, to generate verification results after each unrolling of the next-state relation of the transition system. To this end, we develop a symbolic structural operational semantics (SSOS) for Stateflow, starting from an existing structural operational semantics (SOS), and show the preservation of invariant properties between the two. We define bounded invariant checking for STS over symbolic configurations as a satisfiability problem. We develop an automated procedure for generating the initial and next-state predicates of the STS, and a prototype implementation of the technique in the form of a tool utilising standard, off-the-shelf satisfiability solvers. Finally, we present preliminary performance results by applying our tool on an illustrative example and two industrial models. 

  • 25.
    Guanciale, Roberto
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Privacy preserving business process fusion2015Inngår i: International Workshops on Business Process Management Workshops, BPM 2014, Springer, 2015, Vol. 202, s. 96-101Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Virtual enterprises (VEs) are temporary and loosely coupled alliances of businesses that join their skills to catch new business opportunities. However, the dependencies among the activities of a prospective VE cross the boundaries of the VE constituents. It is therefore crucial to allow the VE constituents to discover their local views of the interorganizational workflow, enabling each company to re-shape, optimize and analyze the possible local flows that are consistent with the processes of the other VE constituents. We refer to this problem asVE process fusion. Even if it has been widely investigated, no previous work addresses VE process fusion in the presence of privacy constraints. In this paper we demonstrate how private intersection of regular languages can be used as the main building block to implement the privacy preserving fusion of business processes modeled by means of bounded Petri nets.

  • 26.
    Guanciale, Roberto
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Laud, P.
    Business process engineering and secure multiparty computation2015Inngår i: Cryptology and Information Security Series, ISSN 1871-6431, Vol. 13, s. 129-149Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    In this chapter we use secure multiparty computation (SMC) to enable privacy-preserving engineering of inter-organizational business processes. Business processes often involve structuring the activities of several organizations, for example when several potentially competitive enterprises share their skills to form a temporary alliance. One of the main obstacles to engineering the processes that govern such collaborations is the perceived threat to the participants’ autonomy. In particular, the participants can be reluctant to expose their internal processes or logs, as this knowledge can be analyzed by other participants to reveal sensitive information. We use SMC techniques to handle two problems in this context: process fusion and log auditing. Process fusion enables the constituents of a collaboration to discover their local views of the inter-organizational workflow, enabling each company to re-shape, optimize and analyze their local flows. Log auditing enables a participant that owns a business process to check if the partner’s logs match its business process, thus enabling the two partners to discover failures, errors and inefficiencies.

  • 27.
    Guanciale, Roberto
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Laud, Peeter
    Private intersection of regular languages2014Inngår i: Privacy, Security and Trust (PST), 2014 Twelfth Annual International Conference on / [ed] Ali Miri, Urs Hengartner, Nen-Fu Huang, Audun Jøsang, Joaquín García-Alfaro, IEEE conference proceedings, 2014, s. 112-120Konferansepaper (Fagfellevurdert)
    Abstract [en]

    This paper addresses the problem of computing the intersection of regular languages in a privacy-preserving fashion. Private set intersection has been addressed earlier in the literature, but for finite sets only. We discuss the various possibilities for solving the problem efficiently, and argue for an approach based on minimal deterministic finite automata (DFA) as a suitable, non-leaking representation of regular language intersection. We propose two different algorithms for DFA minimization in a secure multiparty computation setting, illustrating different aspects of programming based on universal composability and the constraints this sets on existing algorithms. The implementation of our algorithms is based on the programming language SECREC, executing on the SHAREMIND platform for secure multiparty computation. As one application domain we consider fusion of virtual enterprise business processes.

    Fulltekst (pdf)
    pst14.pdf
  • 28.
    Gurov, Dilian
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Goranko, Valentin
    Stockholm Univ, Stockholm, Sweden.;Univ Johannesburg, Inst Intelligent Syst, Soweto, South Africa..
    Lundberg, Edvin
    Rocker AB, Stockholm, Sweden..
    Knowledge-based strategies for multi-agent teams playing against Nature2022Inngår i: Artificial Intelligence, ISSN 0004-3702, E-ISSN 1872-7921, Vol. 309, s. 103728-, artikkel-id 103728Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We study teams of agents that play against Nature towards achieving a common objective. The agents are assumed to have imperfect information due to partial observability, and have no communication during the play of the game. We propose a natural notion of higher-order knowledge of agents. Based on this notion, we define a class of knowledgebased strategies, and consider the problem of synthesis of strategies of this class. We introduce a multi-agent extension, MKBSC, of the well-known knowledge-based subset construction applied to such games. Its iterative applications turn out to compute higherorder knowledge of the agents. We show how the MKBSC can be used for the design of knowledge-based strategy profiles, and investigate the transfer of existence of such strategies between the original game and in the iterated applications of the MKBSC, under some natural assumptions. We also relate and compare the "intensional" view on knowledge-based strategies based on explicit knowledge representation and update, with the "extensional" view on finite memory strategies based on finite transducers and show that, in a certain sense, these are equivalent.

  • 29.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Havelund, Klaus
    Huisman, Marieke
    Monahan, Rosemary
    Static and Runtime Verification, Competitors or Friends?: (Track Summary)2016Inngår i: LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I, 2016, s. 397-401Konferansepaper (Fagfellevurdert)
  • 30.
    Gurov, Dilian
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Herber, P.
    Schaefer, I.
    Automated Verification of Embedded Control Software: Track Introduction2020Inngår i: Leveraging Applications of Formal Methods, Verification and Validation: Applications, Springer Nature , 2020, Vol. 12478, s. 235-239Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Embedded control software is used in a variety of industries, such as in the automotive and railway domains, or in industrial automation and robotization. The development of such software is subject to tight time-to-market requirements, but at the same time also to very high safety requirements posed by various safety standards. To assure the latter, formal methods such as model-based testing and formal verification are increasingly used. However, the main obstacle to a more wide-scale adoption of these methods, and especially of formal verification, is the currently relative low level of automation of the verification process and integration in the general software development cycle. At present, writing formal specifications and annotating the embedded code is still a highly labour intensive activity requiring special competence and skills. In this track we address this challenge from various angles. We start by introducing the topic and then give a summary of the contributions.

  • 31.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, Marieke
    Interface abstraction for compositional verification2005Inngår i: SEFM 2005: Third IEEE International Conference on Software Engineering and Formal Methods, Proceedings / [ed] Aichernig, BK; Beckert, B, 2005, s. 414-423Konferansepaper (Fagfellevurdert)
    Abstract [en]

    To support dynamic loading of applications on portable devices, one needs compositional reasoning techniques to ensure that newly loaded applications cannot break the overall security of a device. In earlier work, we developed an algorithmic verification technique for control flow based safety properties of smart card applications, which allows global system properties to be inferred from the properties of the components. Application of the technique requires knowledge of the names of all methods implemented by these components. In a truly compositional setting, however, one only knows the public interface of the new applet and does not have access to any implementation details. To compositionally verify interface properties of applets, one therefore has to combine our verification technique with an abstraction which preserves the interface behaviour and reduces the set of implemented methods to the set of public methods. In this paper we develop such an abstraction technique: we formally define the notion of interface behaviour and propose an inlining transformation which we prove to preserve the interface properties expressible in our specification language. In addition, we show on a concrete case study how the reduction in the number of methods resulting from the interface abstraction drastically improves the performance of the computationally most expensive step of the compositional verification technique.

  • 32.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, Marieke
    University of Twente, Netherlands .
    Reducing behavioural to structural properties of programs with procedures2013Inngår i: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 480, s. 69-103Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a program graph rather than in terms of its unfoldings is a useful strategy for making analyses more tractable. The present paper presents a characterisation of behavioural program properties through sets of structural properties by means of a translation. The characterisation is given in the context of a program model based on control flow graphs of sequential programs with procedures, abstracting away completely from program data, and properties expressed in a fragment of the modal mu-calculus with boxes and greatest fixed-points only. The property translation is based on a tableau construction that conceptually amounts to symbolic execution of the behavioural formula, collecting structural constraints along the way. By keeping track of the subformulae that have been examined, recursion in the structural constraints can be identified and captured by fixed-point formulae. The tableau construction terminates, and the characterisation is exact, i.e., the translation is sound and complete. A prototype implementation has been developed. In addition, we show how the translation can be extended beyond the basic flow graph model and safety logic to richer behavioural models (such as open programs) and richer program models (including Boolean programs), and discuss possible extensions for more complex logics. We present several applications of the characterisation, in particular sound and complete compositional verification for behavioural properties based on maximal models.

  • 33.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, Marieke
    University of Twente, Netherlands.
    Reducing Behavioural to Structural Properties of Programs with Procedures2009Inngår i: VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION / [ed] Jones ND; MullerOlm M, 2009, Vol. 5403, s. 136-150Konferansepaper (Fagfellevurdert)
    Abstract [en]

    There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a program graph rather than in terms of its unfoldings is a useful strategy for making analyses more tractable. This paper presents a characterisation of behavioural program properties through sets of structural properties by means of a translation. The characterisation is given in the context of a program model based on control flow graphs of sequential programs with possibly recursive procedures, and properties expressed in a fragment of the modal mu-calculus with boxes and greatest fixed-points only. The property translation is based on a tableau construction that conceptually amounts to symbolic execution of the behavioural formula, collecting structural constraints along the way. By keeping track of the subformulae that have been examined, recursion in the structural constraints can be identified and captured by fixed-point formulae. The tableau construction terminates, and the characterisation is exact, i.e., the translation is sound and complete. A prototype implementation has been developed. We discuss several applications of the characterisation, in particular compositional verification for behavioural properties, based on maximal models.

  • 34.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Huisman, Marieke
    Sprenger, Christoph
    Compositional verification of sequential programs with procedures2008Inngår i: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 206, nr 7, s. 840-868Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We present a method for algorithmic, compositional verification of control-flow-based safety properties of sequential programs with procedures. The application of the method involves three steps: (1) decomposing the desired global property into local properties of the components, (2) proving the correctness of the property decomposition by using a maximal model construction, and (3) verifying that the component implementations obey their local specifications. We consider safety properties of both the structure and the behaviour of program control flow. Our compositional verification method builds on a technique proposed by Grumberg and Long that uses maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. We present a novel maximal model construction for the fragment of the modal P-calculus with boxes and greatest fixed points only, and adapt it to control-flow graphs modelling components described in a sequential procedural language. We extend our verification method to programs with private procedures by defining an abstraction, presented as an inlining transformation. All algorithms have been implemented in a tool set automating all required verification steps. We validate our approach on an electronic purse case study.

  • 35.
    Gurov, Dilian
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Hähnle, R.
    Kamburjan, E.
    Who Carries the Burden of Modularity?: Introduction to ISoLA 2020 Track on Modularity and (De-)composition in Verification2020Inngår i: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles: 9th International Symposium on Leveraging, Proceedings, Part I, Springer Nature , 2020, Vol. 12476, s. 3-21Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Modularity and compositionality in verification frameworks occur within different contexts: the model that is the verification target, the specification of the stipulated properties, and the employed verification principle. We give a representative overview of mechanisms to achieve modularity and compositionality along the three mentioned contexts and analyze how mechanisms in different contexts are related. In many verification frameworks one of the contexts carries the main burden. It is important to clarify these relations to understand the potential and limits of the different modularity mechanisms.

  • 36.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Laud, P.
    Guanciale, Roberto
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Privacy preserving business process matching2015Inngår i: 2015 13th Annual Conference on Privacy, Security and Trust, IEEE , 2015, s. 36-43Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Business process matching is the activity of checking whether a given business process can interoperate with another one in a correct manner. In case the check fails, it is desirable to obtain information about how the first process can be corrected with as few modifications as possible to achieve interoperability. In case the two business processes belong to two separate enterprises that want to build a virtual enterprise, business process matching based on revealing the business processes poses a clear threat to privacy, as it may expose sensitive information about the inner operation of the enterprises. In this paper we propose a solution to this problem for business processes described by means of service automata. We propose a measure for similarity between service automata and use this measure to devise an algorithm that constructs the most similar automaton to the first one that can interoperate with the second one. To achieve privacy, we implement this algorithm in the programming language SecreC, executing on the Sharemind platform for secure multiparty computation. As a result, only the correction information is leaked to the first enterprise and no more.

  • 37.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Lidström, Christian
    Scania.
    Nyberg, Mattias
    KTH, Skolan för industriell teknik och management (ITM), Maskinkonstruktion (Inst.), Mekatronik. Systems Development DivisionScania AB, Södertälje, Sweden.
    Westman, Jonas
    KTH, Skolan för industriell teknik och management (ITM), Maskinkonstruktion (Inst.), Mekatronik.
    Deductive Functional Verification of Safety-Critical Embedded C-Code: An Experience Report2017Inngår i: Critical Systems: Formal Methods and Automated Verification, Cham: Springer, 2017, s. 3-18Konferansepaper (Fagfellevurdert)
    Abstract [en]

    This paper summarizes our experiences from an exercise in deductive verification of functional properties of automotive embedded Ccode in an industrial setting. We propose a formal requirements model that supports the way C-code requirements are currently written at Scania. We describe our work, for a safety-critical module of an embedded system, on formalizing its functional requirements and verifying its C-code implementation by means of VCC, an established tool for deductive verification. We describe the obstacles we encountered, and discuss the automation of the specification and annotation effort as a prerequisite for integrating this technology into the embedded software design process.

  • 38.
    Gurov, Dilian
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Lidström, Christian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Rümmer, P.
    Alice in Wineland: A Fairy Tale with Contracts2022Inngår i: The Logic of Software. A Tasting Menu of Formal Methods, Springer Nature , 2022, s. 229-242Kapittel i bok, del av antologi (Fagfellevurdert)
    Abstract [en]

    In this tale Alice ends up in Wineland, where she tries to attend the birthday party of one of its most beloved inhabitants. In order to do so, she must learn about contracts and how important they are. She gets exposed to several contract languages, with their syntax and semantics, such as pre- and post-conditions, state machines, context-free grammars, and interval logic. She learns for what type of properties they are appropriate to use, and how to formally verify that programs meet their contracts.

  • 39.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC).
    Markov, Minko
    Self-Correlation and Maximum Independence in Finite Relations2015Inngår i: Electronic Proceedings in Theoretical Computer Science, E-ISSN 2075-2180, nr 191, s. 60-74Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    We consider relations with no order on their attributes as in Database Theory. An independent partition of the set of attributes S of a finite relation R is any partition (sic) of S such that the join of the projections of R over the elements of (sic) yields R. Identifying independent partitions has many applications and corresponds conceptually to revealing orthogonality between sets of dimensions in multidimensional point spaces. A subset of S is termed self-correlated if there is a value of each of its attributes such that no tuple of R contains all those values. This paper uncovers a connection between independence and self-correlation, showing that the maximum independent partition is the least fixed point of a certain inflationary transformer alpha that operates on the finite lattice of partitions of S. alpha is defined via the minimal self-correlated subsets of S. We use some additional properties of alpha to show the said fixed point is still the limit of the standard approximation sequence, just as in Kleene's well-known fixed point theorem for continuous functions.

  • 40.
    Gurov, Dilian
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Westman, Jonas
    KTH, Skolan för industriell teknik och management (ITM), Maskinkonstruktion (Inst.), Mekatronik. Systems Development Division, Scania AB, Södertälje, Sweden.
    A Hoare Logic Contract Theory: An Exercise in Denotational Semantics2018Inngår i: Principled Software Development: Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday, Springer Nature , 2018, s. 119-127Kapittel i bok, del av antologi (Annet vitenskapelig)
    Abstract [en]

    We sketch a simple theory of Hoare logic contracts for programs with procedures, presented in denotational semantics. In particular, we give a simple semantic justification of the usual procedure-modular treatment of such programs. The justification is given by means of a proof of soundness of a contract-relative denotational semantics against the standard denotational semantics of procedures in the context of procedure declarations. The suggested formal development can be used as an inspiration for more ambitious contract theories.

  • 41.
    Gurov, Dilian
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Østvold, B.M.
    Schaefer, I.
    A hierarchical variability model for software product lines2012Inngår i: Leveraging Applications of Formal Methods, Verification, and Validation: International Workshops, SARS 2011 and MLSC 2011, Held Under the Auspices of ISoLA 2011 in Vienna, Austria, October 17-18, 2011. Revised Selected Papers / [ed] Reiner Hähnle, Jens Knoop, Tiziana Margaria, Dietmar Schreiner, Bernhard Steffen, Springer, 2012, s. 181-199Konferansepaper (Fagfellevurdert)
    Abstract [en]

    A key challenge in software product line engineering is to represent solution space variability in an economic, yet easily understandable fashion. We introduce the notion of hierarchical variability models to describe families of products in a manner that facilitates their modular design and analysis. In this model, a family is represented by a common set of artifacts and a set of variation points with associated variants. A variant is again a hierarchical variability model, leading to a hierarchical structure. These models, however, are not unique with respect to the families they define. We therefore propose a quantitative measure on hierarchical variability models that expresses the degree to which a variability model captures commonality and variability in a family. Further, by imposing well-formedness constraints, we identify a class of variability models that, by construction, have maximal measure and are unique for the families they define. For this class of simple families, we provide a procedure that reconstructs their hierarchical variability model. The reconstructed model can be used to drive various static analyses by divide-and-conquer reasoning. Hierarchical variability models strike a balance between the formalism's expressiveness and the desirable property of model uniqueness. We illustrate the approach by a small product line of Java classes.

  • 42. Huisman, M.
    et al.
    Gurov, Dilian
    KTH.
    Sprenger, C.
    Chugunov, G.
    Checking absence of illicit applet interactions: A case study2004Inngår i: FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS / [ed] Wermelinger, M; MargariaSteffen, T, BERLIN: SPRINGER , 2004, Vol. 2984, s. 84-98Konferansepaper (Fagfellevurdert)
    Abstract [en]

    This paper presents the use of a method - and its corresponding tool set - for compositional verification of applet interactions on a realistic industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus as a test case for formal methods for smart cards. The verification method focuses on the possible interactions between different applets, co-existing on the same card, and provides a technique to specify and detect illicit interactions between these applets. The method is compositional, thus supporting post-issuance loading of applets. The correctness of a global system property can algorithmically be inferred from local applet properties. Later, when loading applets on a card, the implementations are matched against these local properties, in order to guarantee the global property. The theoretical framework underlying our method has been presented elsewhere; the present paper evaluates its practical usability by means of an industrial case study. In particular, we outline the tool set that we have assembled to support the verification process, combining existing model checkers with newly developed tools, tailored to our method.

  • 43. Huisman, Marieke
    et al.
    Aktug, Irem
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Program Models for Compositional Verification2008Inngår i: FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Berlin: Springer , 2008, s. 147-166Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Compositional verification is crucial for guaranteeing the security of systems where new components can be loaded dynamically. In earlier work, we developed a compositional verification principle for control-flow properties of sequential control flow graphs with procedures. This paper discusses how the principle can be generalised to richer program models. We first present a generic program model, of which the original program model is an instantiation, and explicate under what conditions the compositional verification principle applies. We then present two other example instantiations of the generic model: with exceptional and with multi-threaded control flow, and show that for these particular instantiations the conditions hold. The program models we present are specifically tailored to our compositional verification principle, however, they are sufficiently intuitive and standard to be useful on their own. Tool support and practical application of the method are discussed.

  • 44.
    Huisman, Marieke
    et al.
    INRIA Sophia Antipolis, France.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Composing Modal Properties of Programs with Procedures2009Inngår i: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 203, nr 7, s. 87-101Artikkel i tidsskrift (Fagfellevurdert)
    Abstract [en]

    In component based software design, formal reasoning about programs has to be compositional, allowing global, program-wide properties to be inferred from the properties of its components. The present paper addresses the problem of compositional verification of behavioural control flow properties of sequential programs with procedures, expressed in a modal logic. We use as a starting point a maximal model based method previously developed by the authors, which assumes the local properties to be structural (rather than behavioural). To handle local behavioural properties, we propose the combination of the above method with a translation from behavioural properties to sets of structural ones. The present paper presents a direct solution for the logic, and prepares the ground for a translation for the considerably more expressive logic obtained by adding greatest fixed-point recursion.

  • 45.
    Huisman, Marieke
    et al.
    Univ Twente, Enschede, Netherlands.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    CVPP: A Tool Set for Compositional Verification of Control-Flow Safety Properties2011Inngår i: Formal verification of oblect-oriented software / [ed] Beckert, B; Marche, C, 2011, Vol. 6528, s. 107-121Konferansepaper (Fagfellevurdert)
    Abstract [en]

    This paper describes CVPP, a tool set for compositional verification of control-flow safety properties for programs with procedures. The compositional verification principle that underlies CVPP is based on maximal models constructed from component specifications. Maximal models replace the actual components when verifying the whole program, either for the purposes of modularity of verification or due to unavailability of the component implementations at verification time. A characteristic feature of the principle and the tool set is the distinction between program structure and behaviour. While behavioural properties are more abstract and convenient for specification purposes, structural ones are easier to manipulate, in particular when it comes to verification or the construction of maximal models. Therefore, CVPP also contains the means to characterise a given behavioural formula by a set of structural formulae. The paper presents the underlying framework for compositional verification and the components of the tool set. Several verification scenarios are described, as well as wrapper tools that support the automatic execution of such scenarios, providing appropriate pre- and post-processing to interface smoothly with the user and to encapsulate the inner workings of the tool set.

  • 46. Jocevski, Milan
    et al.
    Mardinoglu, Adil
    KTH, Centra, Science for Life Laboratory, SciLifeLab. KTH, Skolan för kemi, bioteknologi och hälsa (CBH), Proteinvetenskap, Systembiologi.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Mohammadat, Tage
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Elektroteknik, Elektronik och inbyggda system.
    Monti, Paolo
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Kommunikationssystem, CoS, Optical Network Laboratory (ON Lab).
    Harmonized Supervision of Degree Project Work2019Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Background and purposeEffective supervision practices are vital for the educational and professional development of students,for continuous growth of supervisors, as well as for the development of respective scientific fields. In lightof different learning styles (Taylor & Beasley 2005) and having in mind the time resource constraints ofsupervisors, it is not easy to point out the best pedagogical approach to supervision that maximizes thelearning experience. In addition to the traditional individual supervision (IS) style there are other options(e.g., group supervision (GS) and peer supervision (PS)), which offer certain advantages. These threestyles do not exclude each other, but can rather be combined to complement each other’s strengths.In order to maximize the effectiveness of combining multiple approaches, it is essential to understand itsadvantages and disadvantages. Based on a survey of different experiences among supervisors andstudents collected from different Swedish education institutions, our paper suggests ways to optimizethe supervision processes. Moreover, we call it harmonized supervision, and belive that it would savetime and effort for the supervisors, and help students to overcome the individual limitations of eachsupervision style. 

    Work done/work in progressIn order to study the preferences of students and supervisors with respect to IS, GS, and PS weconducted a survey among faculty members as well as former students at four higher educationinstitutions (HEIs), where our goal was to aggregate their experiences and learnings. The sampling wasdone in two-stages. First, we selected the HEIs. Due to convenience and connections to specific departments at given HEIs that the authors had, we then sent e-mail invitations to both students andsupervisors at these HEIs. In the second stage, through a voluntary process, respondents from bothgroups took part in the survey. Questions in the survey were inspired by the previous experiences of theauthors, and traditional supervision approaches of the affiliated institutions. We asked informants abouttheir experiences, and what they believed were advantages and disadvantages of each of theexperienced supervision styles. Finally, data was analyzed using descriptive statistics and qualitativeanalysis of open-ended questions. Basically, we looked into which style was used the most and in whichsituations, as well as compared different answers that spoke in favor and against each style.Results/observations/lessons learnedIt is interesting to note that supervisors and students had similar views with respect to IS, GS, and PS. Interms of IS “lack of different perspective” and “limited flows of new idea/opinions” are among thedrawbacks highlighted by both supervisors and students. Interestingly enough, a solution to these issuesis readily available among the benefits of GS and PS, i.e., “New ideas for solving problems” and“Diverse feedback”. This observation leads us to conclude that combining IS, GS, and PS in aharmonized supervision approach. By harmonized supervision we refer to an approach where GS andPS are used as the basis, and where IS is used only when needed.Take-home messageRegardless of the choice of the supervision method, one can note that a mixture of style is moreeffective depending on the learner’s phase, which can be broken down in two main stages. In theinitial phase, the supervisor exercises a more structural and contractual style. For instance, thesupervisor acts as a teacher explaining the research method and the student performs it on a step-bystep basis. The next stage is the training phase, where the supervisor can give the student moreformative assessment support and feedback to develope student's skills until a certain autonomy qualityis achieved. Lastly, the learner becomes a master of the thesis topic and therefore becomes moreindependent. When considering supervision it is important to think about different levels of intellectualdevelopment and the social component of the learning process. At the second phase, i.e. trainingphase, the supervisor can adopt group or peer supervision. Engaging the students in peer and groupsupervision may be conducive to the creation of a more secure learning environment. However, it isessential to provide a constructive group constellation and complementing instructions for peers tomaximize the learning outcomes in an efficient manner.

    Fulltekst (pdf)
    fulltext
  • 47.
    Lidström, Christian
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    An Abstract Contract Theory for Programs with Procedures2021Inngår i: Fundamental Approaches to Software Engineering (FASE 2021) / [ed] Guerra, E Stoelinga, M, Springer Nature , 2021, Vol. 12649, s. 152-171Konferansepaper (Fagfellevurdert)
    Abstract [en]

    When developing complex software and systems, contracts provide a means for controlling the complexity by dividing the responsibilities among the components of the system in a hierarchical fashion. In specific application areas, dedicated contract theories formalise the notion of contract and the operations on contracts in a manner that supports best the development of systems in that area. At the other end, contract meta-theories attempt to provide a systematic view on the various contract theories by axiomatising their desired properties. However, there exists a noticeable gap between the most well-known contract metatheory of Benveniste et al. [5], which focuses on the design of embedded and cyber-physical systems, and the established way of using contracts when developing general software, following Meyer's design-by-contract methodology [18]. At the core of this gap appears to be the notion of procedure: while it is a central unit of composition in software development, the meta-theory does not suggest an obvious way of treating procedures as components. In this paper, we provide a first step towards a contract theory that takes procedures as the basic building block, and is at the same time an instantiation of the meta-theory. To this end, we propose an abstract contract theory for sequential programming languages with procedures, based on denotational semantics. We show that, on the one hand, the specification of contracts of procedures in Hoare logic, and their procedure-modular verification, can be cast naturally in the framework of our abstract contract theory. On the other hand, we also show our contract theory to fulfil the axioms of the meta-theory. In this way, we give further evidence for the utility of the meta-theory, and prepare the ground for combining our instantiation with other, already existing instantiations.

  • 48.
    Lidström, Christian
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Contract Based Embedded Software Design2023Inngår i: Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Proceedings, Springer Nature , 2023, s. 77-94Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In embedded systems development, contract based design is a design paradigm where a system is divided hierarchically into components and developed in a top-down manner, using contracts as a means to divide responsibilities and manage the complexity of the system. Contract theories provide a formal basis for reasoning about the properties of the system, and of the contracts themselves. In previous work, we have developed a contract theory for sequential, procedural programs, that is defined abstractly, at the semantic level. The theory fulfils well-established, desired properties of system design. In this paper, we present a methodology for applying the contract theory in real embedded software design. We show how to instantiate the contract theory with concrete syntaxes for defining components and contracts, and how the contract theory enables formal reasoning about the resulting objects. In order to cope with the need for different behavioural models at different levels of abstraction in an embedded system, we extend the contract theory through parametrisation on the semantic domain. We illustrate the application of the proposed methodology on a small, but realistic example, where the temporal logic TLA is used for reasoning at the system level, while lower level components are specified using pre- and post-conditions in the form of ACSL, a specification language for C.

  • 49. Munoz, D. -J
    et al.
    Pinto, M.
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Fuentes, L.
    Defining categorical reasoning of numerical feature models with feature-wise and variant-wise quality attributes2022Inngår i: 26th ACM International Systems and Software Product Line Conference, SPLC 2022 - Proceedings, Association for Computing Machinery (ACM) , 2022, s. 132-139Konferansepaper (Fagfellevurdert)
    Abstract [en]

    Automatic analysis of variability is an important stage of Software Product Line (SPL) engineering. Incorporating quality information into this stage poses a significant challenge. However, quality-aware automated analysis tools are rare, mainly because in existing solutions variability and quality information are not unified under the same model. In this paper, we make use of the Quality Variability Model (QVM), based on Category Theory (CT), to redefine reasoning operations. We start defining and composing the six most common operations in SPL, but now as quality-based queries, which tend to be unavailable in other approaches. Consequently, QVM supports interactions between variant-wise and feature-wise quality attributes. As a proof of concept, we present, implement and execute the operations as lambda reasoning for CQL IDE - the state-of-the-art CT tool. 

  • 50.
    Munoz, Daniel-Jesus
    et al.
    Univ Malaga, ITIS Software, Malaga, Spain.;Univ Malaga, Dept LCC, Andalucia Tech, CAOSD, Malaga, Spain..
    Gurov, Dilian
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Datavetenskap, Teoretisk datalogi, TCS.
    Pinto, Monica
    Univ Malaga, ITIS Software, Malaga, Spain.;Univ Malaga, Dept LCC, Andalucia Tech, CAOSD, Malaga, Spain..
    Fuentes, Lidia
    Univ Malaga, ITIS Software, Malaga, Spain.;Univ Malaga, Dept LCC, Andalucia Tech, CAOSD, Malaga, Spain..
    Category Theory Framework for Variability Models with Non-functional Requirements2021Inngår i: Advanced Information Systems Engineering (Caise 2021) / [ed] LaRosa, M Sadiq, S Teniente, E, SPRINGER INTERNATIONAL PUBLISHING AG , 2021, Vol. 12751, s. 397-413Konferansepaper (Fagfellevurdert)
    Abstract [en]

    In Software Product Line (SPL) engineering one uses Variability Models (VMs) as input to automated reasoners to generate optimal products according to certain Quality Attributes (QAs). Variability models, however, and more specifically those including numerical features (i.e., NVMs), do not natively support QAs, and consequently, neither do automated reasoners commonly used for variability resolution. However, those satisfiability and optimisation problems have been covered and refined in other relational models such as databases. Category Theory (CT) is an abstract mathematical theory typically used to capture the common aspects of seemingly dissimilar algebraic structures. We propose a unified relational modelling framework subsuming the structured objects of VMs and QAs and their relationships into algebraic categories. This abstraction allows a combination of automated reasoners over different domains to analyse SPLs. The solutions' optimisation can now be natively performed by a combination of automated theorem proving, hashing, balanced-trees and chasing algorithms. We validate this approach by means of the edge computing SPL tool HADAS.

12 1 - 50 of 64
RefereraExporteraLink til resultatlisten
Permanent link
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf