Ändra sökning
Avgränsa sökresultatet
1 - 47 av 47
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Träffar per sida
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sortering
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
  • Standard (Relevans)
  • Författare A-Ö
  • Författare Ö-A
  • Titel A-Ö
  • Titel Ö-A
  • Publikationstyp A-Ö
  • Publikationstyp Ö-A
  • Äldst först
  • Nyast först
  • Skapad (Äldst först)
  • Skapad (Nyast först)
  • Senast uppdaterad (Äldst först)
  • Senast uppdaterad (Nyast först)
  • Disputationsdatum (tidigaste först)
  • Disputationsdatum (senaste först)
Markera
Maxantalet träffar du kan exportera från sökgränssnittet är 250. Vid större uttag använd dig av utsökningar.
  • 1.
    Aceto, Luca
    et al.
    ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS-101 Reykjavik, Iceland.
    Birgisson, Arnar
    Department of Computer Science and Engineering, Chalmers University of Technology, Sweden.
    Ingolfsdottir, Anna
    ICE-TCS, School of Computer Science, Reykjavik University, Menntavegur 1, IS-101 Reykjavik, Iceland.
    Mousavi, Mohammad Reza
    Department of Computer Science, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB Eindhoven, Netherlands.
    Reniers, Michel A.
    Department of Computer Science, Eindhoven University of Technology, P.O. Box 513, NL-5600 MB Eindhoven, Netherlands.
    Rule Formats for Determinism and Idempotence2012Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 77, s. 889-907Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Determinism is a semantic property of (a fragment of) a language that specifies that a program cannot evolve operationally in several different ways. Idempotence is a property of binary composition operators requiring that the composition of two identical specifications or programs will result in a piece of specification or program that is equivalent to the original components. In this paper, we propose (related) meta-theorems for guaranteeing the determinism and idempotence of binary operators. These meta-theorems are formulated in terms of syntactic templates for operational semantics, called rule formats. In order to obtain a powerful rule format for idempotence, we make use of the determinism of certain transition relations in the definition of the format for idempotence. We show the applicability of our formats by applying them to various operational semantics from the literature. © 2010 Elsevier B.V. All rights reserved.

  • 2.
    Aktug, Irem
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Naliuka, Katsiaryna
    University of Trento, Italy.
    ConSpec: A Formal Language for Policy Specification2008Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 74, nr 1-2, s. 2-12Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The paper presents ConSpec, an automata-based policy specification language. The language trades off clean semantics to language expressiveness: a formal semantics for the language is provided as security automata. ConSpec specifications can be used at different stages of the application lifecycle, rendering possible the formalization of various Policy enforcement techniques.

  • 3.
    Araujo, Hugo
    et al.
    Universidade Federal de Pernambuco, Recife, PE, Brazil.
    Carvalho, Gustavo
    Universidade Federal de Pernambuco, Recife, PE, Brazil.
    Mohaqeqi, Morteza
    Uppsala University, Uppsala, Sweden.
    Mousavi, Mohammad Reza
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES). University of Leicester, Leicester, UK.
    Sampaio, Augusto
    Universidade Federal de Pernambuco, Recife, PE, Brazil.
    Sound conformance testing for cyber-physical systems: Theory and implementation2017Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 162, s. 35-54Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Conformance testing is a formal and structured approach to verifying system correctness. We propose a conformance testing algorithm for cyber-physical systems, based on the notion of hybrid conformance by Abbas and Fainekos. We show how the dynamics of system specification and the sampling rate play an essential role in making sound verdicts. We specify and prove error bounds that lead to sound test-suites for a given specification and a given sampling rate. We use reachability analysis to find such bounds and implement the proposed approach using the CORA toolbox in Matlab. We apply the implemented approach on a case study from the automotive domain. © 2017 The Author(s).

  • 4.
    Araujo, Hugo
    et al.
    Univ Fed Pernambuco, Recife, PE, Brazil.
    Carvalho, Gustavo
    Univ Fed Pernambuco, Recife, PE, Brazil.
    Mohaqeqi, Morteza
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Mousavi, Mohammad Reza
    Halmstad Univ, Halmstad, Sweden;Univ Leicester, Leicester, Leics, England.
    Sampaio, Augusto
    Univ Fed Pernambuco, Recife, PE, Brazil.
    Sound conformance testing for cyber-physical systems: Theory and implementation2018Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 162, s. 35-54Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Conformance testing is a formal and structured approach to verifying system correctness. We propose a conformance testing algorithm for cyber-physical systems, based on the notion of hybrid conformance by Abbas and Fainekos. We show how the dynamics of system specification and the sampling rate play an essential role in making sound verdicts. We specify and prove error bounds that lead to sound test-suites for a given specification and a given sampling rate. We use reachability analysis to find such bounds and implement the proposed approach using the CORA toolbox in Matlab. We apply the implemented approach on a case study from the automotive domain.

  • 5.
    Artho, Cyrille
    et al.
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Olveczky, Peter Csaba
    Formal Techniques for Safety-Critical Systems (FTSCS 2014) Preface2017Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 133, s. 89-90Artikel i tidskrift (Övrigt vetenskapligt)
  • 6.
    Artho, Cyrille
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Ölveczky, P.C.
    Formal Techniques for Safety-Critical Systems (FTSCS 2015)2018Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 154, s. 1-2Artikel i tidskrift (Refereegranskat)
  • 7.
    Artho, Cyrille
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Ölveczky, P.C.
    Formal Techniques for Safety-Critical Systems (FTSCS 2016)2019Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 175, s. 35-36Artikel i tidskrift (Refereegranskat)
  • 8.
    Asai, Kenichi
    et al.
    Ochanomizu Univ, Tokyo 112, Japan..
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi. NTUA, Athens, Greece..
    Selected and extended papers from Partial Evaluation and Program Manipulation 2015 (PEPM ' 15)2017Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 137, s. 1-1Artikel i tidskrift (Övrigt vetenskapligt)
  • 9.
    Assmann, Uwe
    Linköpings universitet, Tekniska högskolan. Linköpings universitet, Institutionen för datavetenskap, PELAB - Laboratoriet för programmeringsomgivningar.
    Architectural styles for active documents2005Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 56, nr 1-2, s. 79-98Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    This paper proposes several novel architectural styles for active documents. Active documents are documents that contain not only data, but also servlets, applets, expressions in spreadsheet languages, and other forms of software. To grasp the different forms of architectures, several novel concepts are defined. Invasive document composition is a type-safe form of template expansion and extension, transconsistency is a form of transclusion for architectures, and staged architectures provide a form of staged programming on the architectural level. With these concepts, it is possible to explain the architectures of many document processing applications for Web and office, and we define the architectural styles of wizard-parametrized, script-parametrized, transconsistent, stream-based, and staged active documents. Finally, we give a hypothesis of active document composition: it consists of four elements, namely, explicit architecture, invasiveness, transconsistency, and staging. On the basis of this hypothesis, many applications in Web engineering and document processing get a common background, and can be compared and simplified. © 2004 Elsevier B.V. All rights reserved.

  • 10.
    Beohar, Harsh
    et al.
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
    Cuijpers, Pieter
    Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands.
    Avoiding Diamonds in Desynchronisation2014Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 91, nr PART A, s. 45-69Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The design of concurrent systems often assumes synchronous communication between different parts of a system. When system components are physically apart, this assumption becomes inappropriate. Desynchronisation is a technique that aims to implement a synchronous design in an asynchronous manner by placing buffers between the components of the synchronous design. When queues are used as buffers, the so-called 'diamond property' (among others) ensures correct operation of the desynchronised design. However, this property is difficult to establish in practice. In this paper, we give sufficient and necessary conditions under which a concrete synchronous design (i.e., without the unobservable action) is equivalent to an asynchronous design and formally prove that the diamond property is no longer needed for desynchronisation when half-duplex queues are used as a communication buffer. Furthermore, we discuss how the half-duplex condition can be further relaxed when the diamond property can be partially guaranteed. To illustrate how this theory may be applied, we desynchronise the synchronous systems that are synthesised using supervisory control theory. © 2013 Elsevier B.V.

  • 11.
    Beohar, Harsh
    et al.
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
    Varshosaz, Mahsa
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
    Mousavi, Mohammad Reza
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
    Basic behavioral models for software product lines: Expressiveness and testing pre-orders2016Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 123, s. 42-60Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    In order to provide a rigorous foundation for Software Product Lines (SPLs), several fundamental approaches have been proposed to their formal behavioral modeling. In this paper, we provide a structured overview of those formalisms based on labeled transition systems and compare their expressiveness in terms of the set of products they can specify. Moreover, we define the notion of tests for each of these formalisms and show that our notions of testing precisely capture product derivation, i.e., all valid products will pass the set of test cases of the product line and each invalid product fails at least one test case of the product line. © 2015 The Authors.

  • 12.
    Boudjadar, Abdeldjalil
    et al.
    Linköpings universitet, Institutionen för datavetenskap, Programvara och system. Linköpings universitet, Tekniska fakulteten.
    David, Alexandre
    Aalborg University, Denmark.
    Hyun Kim, Jin
    INRIA IRISA, France.
    Larsen, Kim G.
    Aalborg University, Denmark.
    Mikucionis, Marius
    Aalborg University, Denmark.
    Nyman, Ulrik
    Aalborg University, Denmark.
    Skou, Arne
    Aalborg University, Denmark.
    A reconfigurable framework for compositional schedulability and power analysis of hierarchical scheduling systems with frequency scaling2015Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 113, s. 236-260Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    This paper presents a compositional framework for the modeling and analysis of hierarchical scheduling systems. We consider both schedulability and energy consumption of individual components, while analyzing a single core setting with a voltage frequency scaling CPU. According to the CPU frequency scaling, each task has a set of different execution times. Thus, the energy consumption of the whole system varies from one execution to another. We analyze each component individually by checking the feasibility of its workload against both the CPU availability and energy consumption constraints of such a component. Our periodic task model considers both static and dynamic priorities together with preemptive and non-preemptive behaviors. The models are realized using different forms of Hybrid Automata, all of which are analyzed using variants of UPPAAL. The CPU frequencies, task behavior and scheduling policies used in each component are some of the reconfigurable parameters of the system. Finally, we demonstrate the applicability and scalability of our framework by analyzing the schedulability and power consumption of an avionics system. (C) 2015 Elsevier B.V. All rights reserved.

  • 13.
    Boudjadar, Abdeldjalil
    et al.
    Computer Science, Aalborg University, Denmark.
    David, Alexandre
    Computer Science, Aalborg University, Denmark.
    Hyun Kim, Jin
    Computer Science, Aalborg University, Denmark.
    Larsen, Kim G.
    Computer Science, Aalborg University, Denmark.
    Mikučionis, Marius
    Computer Science, Aalborg University, Denmark.
    Nyman, Ulrik
    Computer Science, Aalborg University, Denmark.
    Skou, Arne
    Computer Science, Aalborg University, Denmark.
    Statistical and exact schedulability analysis of hierarchical scheduling systems2016Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 127, s. 103-130Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    This paper contains two contributions: 1) A development methodology involving two techniques to enhance the resource utilization and 2) a new generic multi-core resource model for hierarchical scheduling systems.

    As the first contribution, we propose a two-stage development methodology relying on the adjustment of timing attributes in the detailed models during the design stage. We use a lightweight method (statistical model checking) for design exploration, easily assuring high confidence in the correctness of the models. Once a satisfactory design has been found, it can be proved schedulable using the computation costly method (symbolic model checking). In order to analyze a hierarchical scheduling system compositionally, we introduce the notion of a stochastic supplier modeling the supply of resources from each component to its child components in the hierarchy. We specifically investigate two different techniques to widen the set of provably schedulable systems: 1) a new supplier model; 2) restricting the potential task offsets.

    We also provide a way to estimate the minimum resource supply (budget) that a component is required to provide. In contrast to analytical methods, we prove non-schedulable cases via concrete counterexamples. By having richer and more detailed scheduling models this framework, has the potential to prove the schedulability of more systems.

    As the second contribution, we introduce a generic resource model for multi-core hierarchical scheduling systems, and show how it can be instantiated for classical resource models: Periodic Resource Models (PRM) and Explicit Deadline Periodic (EDP) resource models. The generic multi-core resource model is presented in the context of a compositional model-based approach for schedulability analysis of hierarchical scheduling systems.

    The multi-core framework presented in this paper is an extension of the single-core framework used for the analysis in the rest of the paper.

  • 14. Broch Johnsen, Einar
    et al.
    Owe, Olaf
    Clarke, Dave
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Bjørk, Joakim
    A formal model of service-oriented dynamic object groups2016Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 115–116, s. 3-22Artikel i tidskrift (Refereegranskat)
  • 15.
    Bygde, Stefan
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Lisper, Björn
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Holsti, Niklas
    Tidorum Ltd, Helsinki, Finland.
    Improved Precision in Polyhedral Analysis with Wrapping2017Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 133, s. 74-87Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Abstract interpretation using convex polyhedra is a common and powerful program analysis technique to discover linear relationships among variables in a program. However, the classical way of performing polyhedral analysis does not model the fact that values typically are stored as xed-size binary strings and usually have wrap-around semantics in the case of over ows. In resource-constrained embedded systems, where 8- or 16-bit processors are used, wrapping behaviour may even be used intentionally to save instructions and execution time. Thus, to analyse such systems accurately and correctly, the wrapping has to be modelled. We present an approach to polyhedral analysis which derives polyhedra that are bounded in all dimensions. Our approach is based on a previously suggested wrapping technique by Simon and King, combined with limited widening, a suitable placement of widening points and size-induced restrictions on unbounded variables. With this method, we can derive fully bounded polyhedra in every step of the analysis. We have implemented our method and Simon and King's method compared them. Our experiments show that for a suite of benchmark programs it gives at least as precise result as Simon and King's method. In some cases we obtain a significantly improved result.

  • 16.
    Carlson, Jan
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik.
    Lisper, Björn
    Mälardalens högskola, Akademin för innovation, design och teknik.
    A resource-efficient event algebra2010Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 75, nr 12, s. 1215-1234Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Events play many roles in computer systems, ranging from hardware interrupts, over event-based software architecture, to monitoring and managing of complex systems. In many applications, however, individual event occurrences are not the main point of concern, but rather the occurrences of certain event patterns. Such event patterns can be defined by means of an event algebra, i.e., expressions representing the patterns of interest are built from simple events and operators such as disjunction, sequence, etc. We propose a novel event algebra with intuitive operators (a claim which is supported by a number of algebraic properties). We also present an efficient detection algorithm that correctly detects any expression with bounded memory, which makes this algebra particularly suitable for resource-constrained applications such as embedded systems.

  • 17. Chilton, Chris
    et al.
    Jonsson, Bengt
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
    Kwiatkowska, Marta
    Compositional assume–guarantee reasoning for input/output component theories2014Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 91, s. 115-137Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We formulate a sound and complete assume-guarantee framework for reasoning compositionally about components modelled as a variant of interface automata. The specification of a component, which expresses both safety and progress properties of input and output interactions with the environment, is characterised by finite traces. The framework supports dynamic reasoning about components and specifications, and includes rules for parallel composition, logical conjunction and disjunction corresponding to independent development, and quotient for incremental synthesis. Practical applicability of the framework is demonstrated through a link layer protocol case study.

  • 18.
    Cicchetti, Antonio
    et al.
    Università degli Studi dell'Aquila, Italia.
    Di Ruscio, Davide
    Università degli Studi dell'Aquila, Italia.
    Decoupling Web Application Concerns through Weaving Operations2008Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 70, nr 1, s. 62-86Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Today's Web applications require instruments and techniques able to face their complexity which has noticeably increased at the expense of productivity and quality factors. A number of design methodologies have been proposed in the process of trying to provide developers with languages and tools to abstract and capture Web applications under orthogonal views, like data, navigation and presentation. While the different modeling language constructs can be unified in a common metamodel, consistency among the distinct concerns is guaranteed by less formal relations. Usually, they are based on name conventions and/or ad hoc tool support that could affect reuse and maintenance ratings of specifications. In order to define rigorous and explicit correspondences between the artifacts produced during a system development, this paper proposes the exploitation of dedicated weaving models. The approach aims at providing structural mappings that do not interfere with the definition of the views on either side achieving a clear separation between them and their connections. Furthermore, following the "everything is a model" principle, this work can enable the use of general-purpose theories and tools. For example, model transformations can be applied to evaluate the given specifications or to derive alternative descriptions like Webile or WebML.

  • 19.
    Dastani, Mehdi
    et al.
    Univ Utrecht, Utrecht, Netherlands..
    Hojjat, Hossein
    Rochester Inst Technol, Rochester, USA..
    Sirjani, Marjan
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. Reykjavik Univ, Reykjavik, Iceland..
    Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2015) Preface2018Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 160, s. 1-2Artikel i tidskrift (Övrigt vetenskapligt)
  • 20.
    de Berardinis, J.
    et al.
    The University of Manchester, School of Computer Science, United Kingdom.
    Forcina, Giorgio
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Jafari, A.
    Reykjavik University, School of Computer Science, Reykjavik, Iceland.
    Sirjani, Marjan
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. University, School of Computer Science, Reykjavik, Iceland.
    Actor-based macroscopic modeling and simulation for smart urban planning2018Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 168, s. 142-164Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Assessing the impacts of a mobility initiative prior to deployment is a complex task for both urban planners and transport companies. Computational models like Tangramob offer an agent-based framework for simulating the evolution of urban traffic after the introduction of new mobility services. However, simulations can be computationally expensive to perform due to their iterative nature and the microscopic representation of traffic. To address this issue, we designed a simplified model architecture of Tangramob in Timed Rebeca (TRebeca) and we developed a tool-chain for the generation runnable instances of this model starting from the same input files of Tangramob. Running TRebeca models allows users to get an idea of how the mobility initiatives under study affect the traveling experience of commuters, in a short time and without the need to use the simulator during this first experimental step. Then, once a subset of these initiatives is identified according to user's criteria, it is reasonable to simulate them with Tangramob in order to get more detailed results. To validate this approach, we compared the output of both the simulator and the TRebeca model on a collection of mobility initiatives. The correlation between the results demonstrates the usefulness of using TRebeca models for unconventional contexts of application.

  • 21.
    de C. Gomes, Pedro
    et al.
    KTH.
    Gurov, Dilian
    KTH.
    Huisman, M.
    Artho, Cyrille
    KTH.
    Specification and verification of synchronization with condition variables2018Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 163, s. 174-189Artikel i tidskrift (Refereegranskat)
    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.

  • 22. Gerakios, Prodromos
    et al.
    Papaspyrou, Nikolaos
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Static safety guarantees for a low-level multithreaded language with regions2014Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 80, nr Part B, s. 223-263Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We present the design of a formal low-level multithreaded language with advanced region-based memory management and thread synchronization primitives, where well-typed programs are memory safe and race free. In our language, regions and locks are combined in a single hierarchy and are subject to uniform ownership constraints imposed by this hierarchical structure: deallocating a region causes its sub-regions to be deallocated. Similarly, when a region is read/write-protected, then its sub-regions inherit the same access rights. We discuss aspects of the integration and implementation of the formal language within Cyclone and evaluate the performance of code produced by the modified Cyclone compiler against highly optimized C programs using pthreads. Our results show that the performance overhead for guaranteed race freedom and memory safety is in most cases acceptable.

  • 23. Giambiagi, P.
    et al.
    Dam, Mads
    KTH, Tidigare Institutioner                               , Data- och systemvetenskap, DSV.
    On the secure implementation of security protocols2004Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 50, nr 3-Jan, s. 73-99Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We consider the problem of implementing a security protocol in such a manner that secrecy of sensitive data is not jeopardized. Implementation is assumed to take place in the context of an API that provides standard cryptography and communication services. Given a dependency specification, stating how API methods can produce and consume secret information, we propose an information flow property based on the idea of invariance under perturbation, relating observable changes in output to corresponding changes in input. Besides the information flow condition itself, the main contributions of the paper are results relating the admissibility property to a direct flow property in the special case of programs which branch on secrets only in cases permitted by the dependency rules. These results are used to derive an unwinding theorem, reducing a behavioural correctness check (strong bisimulation) to an invariant.

  • 24.
    Giambiagi, Pablo
    et al.
    RISE., Swedish ICT, SICS.
    Mads, Dam
    RISE., Swedish ICT, SICS.
    On the Secure Implementation of Security Protocols2004Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 50, nr 1-3, s. 73-99Artikel i tidskrift (Refereegranskat)
  • 25.
    Giantsios, Aggelos
    et al.
    Natl Tech Univ Athens, Sch Elect & Comp Engn, Athens, Greece.
    Papaspyrou, Nikolaos
    Natl Tech Univ Athens, Sch Elect & Comp Engn, Athens, Greece.
    Sagonas, Konstantinos
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi. Natl Tech Univ Athens, Sch Elect & Comp Engn, Athens, Greece.
    Concolic testing for functional languages2017Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 147, s. 109-134Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Concolic testing is a software testing technique that simultaneously combines concrete execution of a program (given specific input, along specific paths) with symbolic execution (generating new test inputs that explore other paths, which gives better path coverage than random test case generation). So far, concolic testing has been applied, mainly at the level of bytecode or assembly code, to programs written in imperative languages that manipulate primitive data types such as integers and arrays. In this article, we demonstrate its application to a functional programming language core, the functional subset of Core Erlang, that supports pattern matching, structured recursive data types such as lists, recursion and higher-order functions. We present CutEr, a tool implementing this testing technique, and describe its architecture, the challenges that it needs to address, its current limitations, and report some experiences from its use.

  • 26.
    Jafari, Ali
    et al.
    Reykjavik Univ, Reykjavik, Iceland.
    Khamespanah, Ehsan
    Reykjavik Univ, Reykjavik, Iceland.
    Sirjani, Marjan
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. Reykjavik Univ, Reykjavik, Iceland.
    Hermanns, Holger
    Univ Saarland, Saarbrucken, Germany..
    Cimini, Matteo
    Indiana Univ, Bloomington, IN, USA..
    PTRebeca: Modeling and analysis of distributed and asynchronous systems2016Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 128, s. 22-50Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Distributed systems exhibit probabilistic and non-deterministic behaviors and may have time constraints. Probabilistic Timed Rebeca (PTRebeca) is introduced as a timed and probabilistic actor-based language for modeling distributed real-time systems with asynchronous message passing. The semantics of PTRebeca is a Timed Markov Decision Process. In this paper, we provide SOS rules for PTRebeca, introduce a new tool-set and describe the corresponding mappings. The tool-set automatically generates a Markov Automaton from a PTRebeca model in the form of the input language of the Interactive Markov Chain Analyzer (IMCA). The IMCA can be used as a back-end model checker for performance analysis of PTRebeca models against expected reachability and probabilistic reachability properties. Comparing to the existing tool-set, proposed in the conference paper, we now have the ability of analyzing significantly larger models, and we also can add different rewards to the model. We show the applicability of our approach and efficiency of our tool by analyzing a Network on Chip architecture as a real-world case study. (C) 2016 Elsevier B.V. All rights reserved.

  • 27.
    Johnson, Pontus
    et al.
    KTH, Skolan för elektro- och systemteknik (EES), Industriella informations- och styrsystem.
    Ekstedt, Mathias
    KTH, Skolan för elektro- och systemteknik (EES), Industriella informations- och styrsystem.
    Goedicke, Michael
    Jacobson, Ivar
    Towards general theories of software engineering2015Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 101, s. 1-5Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The special issue of Science of Computer Programming focuses on the theme of general theories of software engineering. A general theory aims at answering the big questions in its field. Ideally, it should be able to explain and predict important phenomena in the field. A general theory of electromagnetism should help readers to understand why one transformer design is superior to another. Software engineering may be considered by pondering the big questions that general theories of software engineering would address. The software engineering discipline also features a multitude of well-known specific theories in addition to personal general theories.

  • 28. Jongmans, Sung-Shik T. Q.
    et al.
    Clarke, Dave
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Proença, José
    A procedure for splitting data-aware processes and its application to coordination2016Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 115–116, s. 47-78Artikel i tidskrift (Refereegranskat)
  • 29.
    Khakpour, Narges
    et al.
    Tarbiat Modares University, Tehran, Iran.
    Jalili, Saeed
    SRI International, Menlo Park, CA, United States.
    Talcott, Carolyn
    Reykjavík University, Reykjavík, Iceland.
    Sirjani, Marjan
    University of Tehran and IPM, Tehran, Iran.
    Mousavi, Mohammad Reza
    Eindhoven University of Technology, Eindhoven, Netherlands.
    Formal modeling of evolving self-adaptive systems2012Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 78, nr 1, s. 3-26Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    In this paper, we present a formal model, named PobSAM (Policy-based Self-Adaptive Model), for developing and modeling self-adaptive evolving systems. In this model, policies are used as a mechanism to direct and adapt the behavior of self-adaptive systems. A PobSAM model is a collection of autonomous managers and managed actors. The managed actors are dedicated to the functional behavior while the autonomous managers govern the behavior of managed actors by enforcing suitable policies. A manager has a set of configurations including two types of policies: governing policies and adaptation policies. To adapt the system behavior in response to the changes, the managers switch among different configurations. We employ the combination of an algebraic formalism and an actor-based model to specify this model formally. Managed actors are expressed by an actor model. Managers are modeled as meta-actors whose configurations are described using a multi-sorted algebra called CA. We provide an operational semantics for PobSAM using labeled transition systems. Furthermore, we provide behavioral equivalence of different sorts of CA in terms of splitting bisimulation and prioritized splitting bisimulation. Equivalent managers send the same set of messages to the actors. Using our behavioral equivalence theory, we can prove that the overall behavior of the system is preserved by substituting a manager by an equivalent one. © 2011 Elsevier B.V. All rights reserved.

  • 30.
    Khakpour, Narges
    et al.
    Tarbiat Modares University, Iran.
    Jalili, Saeed
    Tarbiat Modares University, Iran.
    Talcott, Carolyn
    SRI International, United States.
    Sirjani, Marjan
    Reykjavík University, Iceland.
    Mousavi, MohammadReza
    Eindhoven University of Technology, The Netherlands.
    Formal modeling of evolving self-adaptive systems2012Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 78, nr 1, s. 3-26Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    In this paper, we present a formal model, named PobSAM (Policy-based Self-Adaptive Model), for developing and modeling self-adaptive evolving systems. In this model, policies are used as a mechanism to direct and adapt the behavior of self-adaptive systems. A PobSAM model is a collection of autonomous managers and managed actors. The managed actors are dedicated to the functional behavior while the autonomous managers govern the behavior of managed actors by enforcing suitable policies. A manager has a set of configurations including two types of policies: governing policies and adaptation policies. To adapt the system behavior in response to the changes, the managers switch among different configurations. We employ the combination of an algebraic formalism and an actor-based model to specify this model formally. Managed actors are expressed by an actor model. Managers are modeled as meta-actors whose configurations are described using a multi-sorted algebra called CA. We provide an operational semantics for PobSAM using labeled transition systems. Furthermore, we provide behavioral equivalence of different sorts of CA in terms of splitting bisimulation and prioritized splitting bisimulation. Equivalent managers send the same set of messages to the actors. Using our behavioral equivalence theory, we can prove that the overall behavior of the system is preserved by substituting a manager by an equivalent one.

  • 31.
    Khamespanah, E.
    et al.
    School of Electrical an Computer Engineering, University of Tehran, Tehran, Iran.
    Khosravi, R.
    School of Computer Science, Reykjavik University, Reykjavik, Iceland.
    Sirjani, Marjan
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    An efficient TCTL model checking algorithm and a reduction technique for verification of timed actor models2018Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 153, s. 1-29Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    NP-hard time complexity of model checking algorithms for TCTL properties in dense time is one of the obstacles against using model checking for the analysis of real-time systems. Alternatively, a polynomial time algorithm is suggested for model checking of discrete time models against TCTL≤,≥ properties (i.e. TCTL properties without U=c modalities). The algorithm performs model checking against a given formula Φ for a state space with V states and E transitions in O(V(V+E)⋅|Φ|). In this work, we improve the model checking algorithm of TCTL≤,≥ properties, obtaining time complexity of O((Vlg⁡V+E)⋅|Φ|). We tackle the model checking of discrete timed actors as an application of the proposed algorithms. We show how the result of the fine-grained semantics of discrete timed actors can be model checked efficiently against TCTL≤,≥ properties using the proposed algorithm. This is illustrated using the timed actor modeling language Timed Rebeca. In addition to introducing a new efficient model checking algorithm, we propose a reduction technique which safely eliminates instantaneous transitions of transition systems (i.e. transition with zero time duration). We show that the reduction can be applied on-the-fly during the generation of the original timed transition system without a significant cost. We demonstrate the effectiveness of the reduction technique via a set of case studies selected from various application domains. Besides, while TCTL≤,≥ can be model checked in polynomial time, model checking of TCTL properties with U=c modalities is an NP-complete problem. Using the proposed reduction technique, we provide an efficient algorithm for model checking of complete TCTL properties over the reduced transition systems.

  • 32.
    Lang, Frédéric
    et al.
    Université de Grenoble Alpes, France.
    Flammini, Francesco
    Ansaldo STS, Italy.
    Preface to the special issue on Formal Methods for Industrial Critical Systems (FMICS'2014)2016Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 118, s. 1-2Artikel i tidskrift (Refereegranskat)
  • 33.
    Lengauer, Christian
    et al.
    University of Passau, Germany.
    Taha, Walid
    Rice University, Computer Science, Houston, United States.
    Preface2006Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 62, nr 1, s. 1-2Artikel i tidskrift (Övrigt vetenskapligt)
  • 34.
    Lindner, Andreas
    et al.
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Guanciale, Roberto
    KTH, Skolan för elektroteknik och datavetenskap (EECS), Teoretisk datalogi, TCS.
    Metere, R.
    TrABin: Trustworthy analyses of binaries2019Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 174, s. 72-89Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Verification of microkernels, device drivers, and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: the adoption of hardware-independent intermediate representations, a mechanism to translate architecture dependent code to this representation, and a set of architecture independent analyses that process the intermediate representation. The usage of these platforms to verify software introduces the need for trusting both the correctness of the translation from binary code to intermediate language (called transpilation) and the correctness of the analyses. Achieving a high degree of trust is challenging since the transpilation must handle (i) all the side effects of the instructions, (ii) multiple instruction encodings (e.g. ARM Thumb), and (iii) variable instruction length (e.g. Intel). Similarly, analyses can use complex transformations (e.g. loop unrolling) and simplifications (e.g. partial evaluation) of the artifacts, whose bugs can jeopardize correctness of the results. We overcome these problems by developing a binary analysis platform on top of the interactive theorem prover HOL4. First, we formally model a binary intermediate language and we prove correctness of several supporting tools (i.e. a type checker). Then, we implement two proof-producing transpilers, which respectively translate ARMv8 and CortexM0 programs to the intermediate language and generate a certificate. This certificate is a HOL4 proofdemonstrating correctness of the translation. As demonstrating analysis, we implement a proof-producing weakest precondition generator, which can be used to verify that a given loop-free program fragment satisfies a contract. Finally, we use an AES encryption implementation to benchmark our platform.

  • 35.
    Mousavi, Mohammad Reza
    et al.
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
    Pang, Jun
    University of Luxembourg, Luxembourg, Luxembourg.
    Special section on Software Verification and Testing2014Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 95, Part 3, s. 273-274Artikel i tidskrift (Övrigt vetenskapligt)
  • 36.
    Mousavi, Mohammad Reza
    et al.
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
    Ravara, Antonio
    Department of Informatics, Faculty of Sciences and Technology, New University of Lisbon, Portugal.
    Foreword: Special issue on the 10th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA 2011)2014Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 89, s. 68s. 1-1Artikel i tidskrift (Övrigt vetenskapligt)
  • 37.
    Nordlander, Johan
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Polymorphic subtyping in O'Haskell2002Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 43, nr 2-3, s. 93-127Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    O'Haskell is a programming language derived from Haskell by the addition of concurrent reactive objects and subtyping. Because Haskell already encompasses an advanced type system with polymorphism and overloading, the type system of O'Haskell is much richer than what is the norm in almost any widespread object-oriented or functional language. Yet, there is strong evidence that O'Haskell is not a complex language to use, and that both Java and Haskell programmers can easily find their way with its polymorphic subtyping system. This paper describes the type system of O'Haskell both formally and from a programmer's point of view; the latter task is accomplished with the aid of an illustrative, real-world programming example: a strongly typed interface to the graphical toolkit Tk.

  • 38.
    Proenca, Jose
    et al.
    Univ Minho, Dept Informat, P-4710057 Braga, Portugal;INESC TEC, P-4710057 Braga, Portugal.
    Clarke, Dave
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Typed connector families and their semantics2017Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 146, s. 28-49Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Typed models of connector/component composition specify interfaces describing ports of components and connectors. Typing ensures that these ports are plugged together appropriately, so that data can flow out of each output port and into an input port. These interfaces typically consider the direction of data flow and the type of values flowing. Components, connectors, and systems are often parameterised in such a way that the parameters affect the interfaces. Typing such connector families is challenging. This paper takes a first step towards addressing this problem by presenting a calculus of connector families with integer and boolean parameters. The calculus is based on monoidal categories, with a dependent type system that describes the parameterised interfaces of these connectors. We use families of Reo connectors as running examples, and show how this calculus can be applied to Petri Nets and to BIP systems. The paper focuses on the structure of connectors-well-connectedness-and less on their behaviour, making it easily applicable to a wide range of coordination and component-based models. A type-checking algorithm based on constraints is used to analyse connector families, supported by a proof of-concept implementation.

  • 39.
    Päivärinta, Tero
    et al.
    Luleå tekniska universitet, Institutionen för system- och rymdteknik, Datavetenskap.
    Smolander, Kari
    Lappeenranta University of Technology.
    Theorizing about Software Development Practices2015Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 101, s. 124-135Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The paper focuses on the challenge of generating theoretical support for software development, especially when human software developers are involved in the software development process. We outline a model, “Coat Hanger”, for theorizing about development practices. The model focuses on the intended rationale for the actual realization and resulting impacts of using particular practices in varying contexts. To illustrate the use of the model, we have studied recent practice-oriented articles in the journal Science of Computer Programming. A survey of articles in the journal between 2010 and 2013 showed that out of 371 articles, only four studied software development in professional organizations with actual software practitioners as informants. The Coat Hanger model was then used to identify the theoretical strengths and weaknesses of these four practice descriptions. The analysis is used as the basis to declare the potential of our model as a conceptual aid for more structured theorizing about software development practices. The contribution of the model is the introduction of a concretization of how theorizing can be done through reflection-in-action, instead of regarding research on software practices plainly from the prevailing viewpoint of technical rationality.

  • 40.
    Sagonas, Konstantinos
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Wilhelmsson, Jesper
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Efficient Memory Management for Concurrent Programs that Use Message Passing2006Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 62, nr 2, s. 98-121Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We present an efficient memory management scheme for concurrent programming languages where communication occurs using message passing with copying semantics. The runtime system is built around process-local heaps, which frees the memory manager from redundant synchronization in a multi-threaded implementation and allows the memory reclamation of process-local heaps to be a private business and to often take place without ever triggering garbage collection. The allocator is guided by a static analysis which speculatively allocates data possibly used as messages in a shared memory area.

    To respect the (soft) real-time requirements of the language, we develop and present in detail a generational, incremental garbage collection scheme tailored to the characteristics of this runtime system. The incremental collector imposes no overhead on the mutator, requires no costly barrier mechanisms, has a relatively small space overhead and can be scheduled either based on a time or on a work quantum.

    We have implemented these schemes in the context of an industrial-strength implementation of a concurrent functional language used to develop large-scale, highly concurrent, telecommunication applications. Our measurements across a range of applications indicate that the incremental collector imposes only very small overhead on the total runtime, can achieve very short pause times (1 millisecond or less) while being able to sustain a high degree of mutator utilization.

  • 41.
    Seceleanu, Cristina Cerschi
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Johansson, M.
    ABB Corporate Research, Sweden.
    Suryadevara, J.
    Volvo Construction Equipment, Sweden.
    Sapienza, Gaetana
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. ABB Corporate Research, Sweden.
    Seceleanu, Tiberiu
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. ABB Corporate Research, Sweden.
    Ellevseth, S. -E
    ABB Corporate Research, Norway.
    Pettersson, Paul
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system.
    Analyzing a wind turbine system: From simulation to formal verification2017Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 133, s. 216-242Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Many industrial systems are hybrid by nature, most often being made of a discrete controller that senses and regulates the execution of a plant characterized by continuous dynamics. Examples of such systems include wind turbines that convert wind energy into electrical energy. Designing industrial control systems is challenging, due to the mixed nature of requirements (functional, timing, etc.) as well as due to the complexity stemming from the interaction of the controller with the plant. Model-based techniques help in tackling the design challenges, whereas methods such as simulation with tools like MATLAB/Simulink can be employed for analysis. Although practical, these methods alone cannot ensure full predictability, due to the fact that they cannot guarantee system properties for all possible executions of the system model. In order to ensure that the system will behave as expected under any operational circumstance, formal verification and validation procedures need to be added to the actual development process. In this paper, we propose an extension of the iFEST (industrial Framework for Embedded Systems Tools) process and platform for embedded systems design with model-based testing using MaTeLo, and model checking time-dependent requirements with the UPPAAL tool, as means of increasing the confidence in the system's behavior. To show the feasibility of the techniques on industrially-sized systems, we analyze a wind turbine industrial prototype model against functional and timing requirements. We capture the execution semantics of the plant and controller components of the wind turbine via logical clocks and constraints expressed in the clock constraint specification language (CCSL) of UML MARTE, after which we construct real-time models amenable to model checking, by mapping the timed behavior (expressed in CCSL) of the real-time components of the wind turbine, onto timed automata. Our work is a first application on an industrial wind turbine system of complementary methods for formal analysis, that is, model-based testing, and model checking a mathematically tractable system abstraction based on data obtained by simulating the system with MATLAB/Simulink. We also discuss relevant modeling and verification challenges encountered during our experiences with the wind turbine system.

  • 42. Soleimanifard, Siavash
    et al.
    Gurov, Dilian
    Algorithmic verification of procedural programs in the presence of code variability2016Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 127, s. 76-102Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    We present a generic framework for verifying temporal safety properties of procedural programs that are dynamically or statically configured by replacing, adapting, or adding new components. To deal with such a variability of a program, we require programmers to provide local specifications for its variable components, and verify the global properties by replacing these specifications with maximal models. Our framework is a generalization of a previously developed framework that fully abstracts from program data. In this work, we recapture program data and thus significantly increase the range of properties that can be verified. Our framework is generic by being parametric on the set of observed program events and their semantics. We separate program structure from the behaviour it induces to facilitate independent component specification and verification. To exemplify the use of the framework, we develop three concrete instantiations; in particular, we derive a compositional verification technique for programs written in a procedural language with pointers as the only datatype.

  • 43.
    Solin, Kim
    et al.
    Uppsala universitet, Humanistisk-samhällsvetenskapliga vetenskapsområdet, Historisk-filosofiska fakulteten, Filosofiska institutionen, Avdelningen för teoretisk filosofi.
    von Wright, Joakim
    Enabledness and termination in refinement algebra2009Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 74, nr 8, s. 654-668Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Refinement algebras are abstract algebras for reasoning about programs in a total correctness framework. We extend a reduct of von Wright's demonic refinement algebra with two operators for modelling enabledness and termination of programs. We show how the operators can be used for expressing relations between programs and apply the algebra to reasoning about action systems.

  • 44.
    Stoica, Anca-Juliana
    et al.
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datalogi.
    Pelckmans, Kristiaan
    Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Avdelningen för systemteknik. Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Reglerteknik.
    Rowe, William
    System components of a general theory of software engineering2015Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 101, s. 42-65Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    The contribution of this paper to a general theory of software engineering is twofold: it presents the model system concept, and it integrates the software engineering design process into a decision making theory and a value-based decision-under-risk process. The model system concept is defined as a collection of interconnected and consistent components that work together for defining, developing, and delivering a software system. This model system concept is used to represent the multiple facets of a software engineering project such as stakeholders and models related to domain/environment, success, decision, product, process, and property. The model system concept is derived from software development practices in the industry and academia. The theoretical decision framework acts as a central governance component for a given software engineering project. Applying this decision framework allows for effectively managing risks and uncertainties related to success in the project building stage. Especially, this puts the design process in an economic perspective, where concepts such as value-of-waiting, value-of-information and possible outcomes can be coped with explicitly. In practice, the decision framework allows for the optimal control of modern adaptive software development. In particular, one can use dynamic programming to find the optimal sequence of decisions to be made considering a defined time horizon. In this way we can relate our contribution to a theory of software engineering to the well-studied areas of automatic control, optimization, decision theory and Bayesian analysis.

  • 45.
    UL Muram, Faiz
    et al.
    Mälardalens högskola, Akademin för innovation, design och teknik, Inbyggda system. University of Vienna, Vienna, Austria.
    Tran, H.
    University of Vienna, Vienna, Austria.
    Zdun, U.
    University of Vienna, Vienna, Austria.
    Supporting automated containment checking of software behavioural models using model transformations and model checking2019Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 174, s. 38-71Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    Models are extensively used in many areas of software engineering to represent the behaviour of software systems at different levels of abstraction. Because of the involvement of different stakeholders in constructing these models and their independent evolution, inconsistencies might occur between the models. It is thus crucial to detect these inconsistencies at early phases of the software development process, and especially as soon as refined models deviate from their abstract counterparts. In this article, we introduce a containment checking approach to verify whether a certain low-level behaviour model, typically created by refining and enhancing a high-level model, still is consistent with the specification provided in its high-level counterpart. We interpret the containment checking problem as a model checking problem, which has not received special treatment in the literature so far. Because the containment checking is based on model checking, it requires both formal consistency constraints and specifications of these models. Unfortunately, creating formal consistency constraints and specifications is currently done manually, and therefore, labour-intensive and error prone. To alleviate this issue, we define and develop a fully automated transformation of behaviour models into formal specifications and properties. The generated formal specifications and properties can directly be used by existing model checkers for detecting any discrepancy between the input models and yield corresponding counterexamples. Moreover, our approach can provide the developers more informative and comprehensive feedback regarding the inconsistency issues, and therefore, help them to efficiently identify and resolve the problems. The evaluation of various scenarios from industrial case studies demonstrates that the proposed approach efficiently translates the behaviour models into formal specifications and properties. 

  • 46.
    Varshosaz, Mahsa
    et al.
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
    Beohar, Harsh
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
    Mousavi, Mohammad Reza
    Högskolan i Halmstad, Akademin för informationsteknologi, Halmstad Embedded and Intelligent Systems Research (EIS), Centrum för forskning om inbyggda system (CERES).
    Basic Behavioral Models For Software Product Lines: Revisited2018Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 168, s. 171-185Artikel i tidskrift (Övrigt vetenskapligt)
    Abstract [en]

    In Beohar et al. (2016) [9], we established an expressiveness hierarchy and studied the notions of refinement and testing for three fundamental behavioral models for software product lines. These models were featured transition systems, product line labeled transition systems, and modal transition systems. It turns out that our definition of product line labeled transition systems is more restrictive than the one introduced by Gruler, Leucker, and Scheidemann. Adopting the original and more liberal notion changes the expressiveness results, as we demonstrate in this paper. Namely, we show that the original notion of product line labeled transition systems and featured transition systems are equally expressive. As an additional result, we show that there are featured transition systems for which the size of the corresponding product line labeled transition system, resulting from any sound encoding, is exponentially larger than the size of the original model. Furthermore, we show that each product line labeled transition system can be encoded into a featured transition system, such that the size of featured transition system is linear in terms of the size of the corresponding model. To summarize, featured transition systems are equally expressive as, but exponentially more succinct than, product line labeled transition systems. © 2018 Elsevier B.V.

  • 47.
    Westman, Jonas
    et al.
    KTH, Skolan för industriell teknik och management (ITM), Maskinkonstruktion (Inst.), Mekatronik.
    Nyberg, Mattias
    KTH, Skolan för industriell teknik och management (ITM), Maskinkonstruktion (Inst.), Mekatronik.
    Gustavsson, Joakim
    KTH, Skolan för industriell teknik och management (ITM), Maskinkonstruktion (Inst.), Mekatronik.
    Gurov, Dilian
    KTH, Skolan för datavetenskap och kommunikation (CSC), Teoretisk datalogi, TCS.
    Formal Architecture Modeling of Sequential Non-Recursive C Programs2017Ingår i: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 146, s. 2-27Artikel i tidskrift (Refereegranskat)
    Abstract [en]

    To manage the complexity of C programs, architecture models are used as high-level descriptions, allowing developers to understand, assess, and manage the C programs without having to understand the intricate complexity of the code implementations. However, for the architecture models to serve their purpose, they must be accurate representations of the C programs. In order to support creating accurate architecture models, the present paper presents a mapping from the domain of sequential non-recursive C programs to a domain of formal architecture models, each being a hierarchy of components with well-defined interfaces. The hierarchically organized components and their interfaces, which capture both data and function call dependencies, are shown to both enable high-level assessment and analysis of the C program and provide a foundation for organizing and expressing specifications for compositional verification.

1 - 47 av 47
RefereraExporteraLänk till träfflistan
Permanent länk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf