Change search
Link to record
Permanent link

Direct link
BETA
Publications (10 of 38) Show all publications
de C. Gomes, P., Gurov, D., Huisman, M. & Artho, C. (2018). Specification and verification of synchronization with condition variables. Science of Computer Programming, 163, 174-189
Open this publication in new window or tab >>Specification and verification of synchronization with condition variables
2018 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 163, p. 174-189Article in journal (Refereed) Published
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.

Place, publisher, year, edition, pages
Elsevier, 2018
Keywords
Concurrency, Condition variables, Formal verification, Java
National Category
Computer Systems
Identifiers
urn:nbn:se:kth:diva-228693 (URN)10.1016/j.scico.2018.05.001 (DOI)000438662800011 ()2-s2.0-85047065786 (Scopus ID)
Funder
EU, European Research Council, 258405
Note

QC 20180530

Available from: 2018-05-30 Created: 2018-05-30 Last updated: 2018-08-03Bibliographically approved
Oortwijn, W., Blom, S., Gurov, D., Huisman, M. & Zaharieva-Stojanovski, M. (2017). An Abstraction Technique for Describing Concurrent Program Behaviour. In: 9th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017: . Paper presented at 9th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017, Heidelberg, Germany, 22 July 2017 through 23 July 2017 (pp. 191-209). Springer, 10712
Open this publication in new window or tab >>An Abstraction Technique for Describing Concurrent Program Behaviour
Show others...
2017 (English)In: 9th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017, Springer, 2017, Vol. 10712, p. 191-209Conference paper, Published paper (Refereed)
Abstract [en]

This paper presents a technique to reason about functional properties of shared-memory concurrent software by means of abstraction. The abstract behaviour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show that the concrete program steps adhere to this specification. Separately, we also use program logics to prove that the program behaves as described by the process algebra term. Finally, via process algebraic reasoning we derive properties that hold for the program from its abstraction. This technique allows reasoning about the behaviour of highly concurrent, non-deterministic and possibly non-terminating programs. The paper discusses various verification examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool support.

Place, publisher, year, edition, pages
Springer, 2017
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10712
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-224402 (URN)10.1007/978-3-319-72308-2_12 (DOI)2-s2.0-85041435817 (Scopus ID)9783319723075 (ISBN)
Conference
9th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2017, Heidelberg, Germany, 22 July 2017 through 23 July 2017
Note

QC 20180316

Available from: 2018-03-16 Created: 2018-03-16 Last updated: 2018-03-16Bibliographically approved
De Carvalho Gomes, P., Gurov, D. & Huisman, M. (2017). Specification and verification of synchronization with condition variables. In: 5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016: . Paper presented at 5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016, Tokyo, Japan, 14 November 2016 through 15 November 2016 (pp. 3-19). Springer, 694
Open this publication in new window or tab >>Specification and verification of synchronization with condition variables
2017 (English)In: 5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016, Springer, 2017, Vol. 694, p. 3-19Conference paper, Published paper (Refereed)
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.

Place, publisher, year, edition, pages
Springer, 2017
Series
Communications in Computer and Information Science, ISSN 1865-0929 ; 694
Keywords
Computer software, Explosions, Extraction, Petri nets, Safety engineering, Security systems, Specifications, Synchronization, Automated extraction, Combinatorial explosion, Concurrent program, Imperative languages, Liveness properties, Parallel Computation, Reachability problem, Specification and verification, Java programming language
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-207406 (URN)10.1007/978-3-319-53946-1_1 (DOI)000406995100001 ()2-s2.0-85013324816 (Scopus ID)9783319539454 (ISBN)
Conference
5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016, Tokyo, Japan, 14 November 2016 through 15 November 2016
Note

QC 20170530

Available from: 2017-05-30 Created: 2017-05-30 Last updated: 2018-01-13Bibliographically approved
Gurov, D., Havelund, K., Huisman, M. & Monahan, R. (2016). Static and Runtime Verification, Competitors or Friends?: (Track Summary). In: LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I. Paper presented at 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), OCT 10-14, 2016, Corfu, GREECE (pp. 397-401).
Open this publication in new window or tab >>Static and Runtime Verification, Competitors or Friends?: (Track Summary)
2016 (English)In: LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I, 2016, p. 397-401Conference paper, Published paper (Refereed)
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9952
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-199816 (URN)10.1007/978-3-319-47166-2_27 (DOI)000389939100027 ()2-s2.0-84994048591 (Scopus ID)978-3-319-47166-2; 978-3-319-47165-5 (ISBN)
Conference
7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), OCT 10-14, 2016, Corfu, GREECE
Note

QC 20170116

Available from: 2017-01-16 Created: 2017-01-16 Last updated: 2018-01-13Bibliographically approved
Soleimanifard, S. & Gurov, D. (2015). Algorithmic verification of procedural programs in the presence of code variability. In: Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers. Paper presented at 11th International Symposium on Formal Aspects of Component Software, FACS 2014, Bertinoro, Italy, 10 September 2014 through 12 September 2014 (pp. 327-345). Springer, 8997
Open this publication in new window or tab >>Algorithmic verification of procedural programs in the presence of code variability
2015 (English)In: Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers, Springer, 2015, Vol. 8997, p. 41p. 327-345Conference paper, Published paper (Refereed)
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 abstracts from all program data. In this work, we capture 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 behavior it induces to facilitate independent component specification and verification. We provide tool support for an instantiation of our framework to programs written in a procedural language with pointers as the only datatype.

Place, publisher, year, edition, pages
Springer, 2015. p. 41
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 8997
Keywords
Algorithms, Computer software, Semantics, Algorithmic verification, Generic frameworks, Global properties, Independent components, New components, Procedural languages, Program structures, Temporal safety properties
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-128950 (URN)10.1007/978-3-319-15317-9_20 (DOI)2-s2.0-84922326750 (Scopus ID)978-3-319-15316-2 (ISBN)978-3-319-15317-9 (ISBN)
Conference
11th International Symposium on Formal Aspects of Component Software, FACS 2014, Bertinoro, Italy, 10 September 2014 through 12 September 2014
Note

QC 20150504. Updated from manuscript to conference paper.

Available from: 2013-09-17 Created: 2013-09-17 Last updated: 2018-01-11Bibliographically approved
de Carvalho Gomes, P., Gurov, D. & Huisman, M. (2015). Algorithmic Verification of Synchronization with Condition Variables.
Open this publication in new window or tab >>Algorithmic Verification of Synchronization with Condition Variables
2015 (English)Report (Other academic)
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

Publisher
p. 26
Keywords
Concurrency, Formal Verification, Coloured Petri Nets, Java
National Category
Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-176006 (URN)
Note

QC 20160517

Available from: 2015-10-27 Created: 2015-10-27 Last updated: 2016-05-24Bibliographically approved
Guanciale, R., Gurov, D. & Laud, P. (2015). Business process engineering and secure multiparty computation. Cryptology and Information Security Series, 13, 129-149
Open this publication in new window or tab >>Business process engineering and secure multiparty computation
2015 (English)In: Cryptology and Information Security Series, ISSN 1871-6431, Vol. 13, p. 129-149Article in journal (Refereed) Published
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.

Place, publisher, year, edition, pages
IOS Press, 2015
National Category
Other Mechanical Engineering
Identifiers
urn:nbn:se:kth:diva-174656 (URN)10.3233/978-1-61499-532-6-129 (DOI)2-s2.0-84957946794 (Scopus ID)
Note

QC 20151130

Available from: 2015-11-30 Created: 2015-10-07 Last updated: 2015-11-30Bibliographically approved
Guanciale, R. & Gurov, D. (2015). Privacy preserving business process fusion. In: International Workshops on Business Process Management Workshops, BPM 2014: . Paper presented at International Workshops on Business Process Management Workshops, BPM 2014, Eindhoven, Netherlands, 7 September 2014 through 8 September 2014 (pp. 96-101). Springer, 202
Open this publication in new window or tab >>Privacy preserving business process fusion
2015 (English)In: International Workshops on Business Process Management Workshops, BPM 2014, Springer, 2015, Vol. 202, p. 96-101Conference paper, Published paper (Refereed)
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.

Place, publisher, year, edition, pages
Springer, 2015
Series
Lecture Notes in Business Information Processing, ISSN 1865-1348 ; 202
Keywords
Business process fusion, Petri nets, Privacy, SMC
National Category
Economics and Business Computer and Information Sciences
Identifiers
urn:nbn:se:kth:diva-170485 (URN)10.1007/978-3-319-15895-2_9 (DOI)2-s2.0-84929916153 (Scopus ID)978-331915894-5 (ISBN)
Conference
International Workshops on Business Process Management Workshops, BPM 2014, Eindhoven, Netherlands, 7 September 2014 through 8 September 2014
Note

QC 20150701

Available from: 2015-07-01 Created: 2015-07-01 Last updated: 2018-01-11Bibliographically approved
Gurov, D., Laud, P. & Guanciale, R. (2015). Privacy preserving business process matching. In: 2015 13th Annual Conference on Privacy, Security and Trust: . Paper presented at 13th Annual Conference on Privacy, Security and Trust, PST 2015; Izmir; Turkey (pp. 36-43). IEEE
Open this publication in new window or tab >>Privacy preserving business process matching
2015 (English)In: 2015 13th Annual Conference on Privacy, Security and Trust, IEEE , 2015, p. 36-43Conference paper, Published paper (Refereed)
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.

Place, publisher, year, edition, pages
IEEE, 2015
Keywords
Automata theory, Virtual corporation, Business Process, Privacy preserving, Secure multi-party computation, Sensitive informations, Service automata, Virtual enterprise, Data privacy
National Category
Information Systems
Identifiers
urn:nbn:se:kth:diva-187122 (URN)10.1109/PST.2015.7232952 (DOI)000375692700006 ()2-s2.0-84958659600 (Scopus ID)978-146737828-4 (ISBN)
Conference
13th Annual Conference on Privacy, Security and Trust, PST 2015; Izmir; Turkey
Note

QC 20160519

Available from: 2016-05-19 Created: 2016-05-17 Last updated: 2018-01-10Bibliographically approved
Amighi, A., de Carvalho Gomes, P., Gurov, D. & Huisman, M. (2015). Provably Correct Control Flow Graphs from Java Bytecode Programs with Exceptions. International Journal on Software Tools for Technology Transfer (STTT)
Open this publication in new window or tab >>Provably Correct Control Flow Graphs from Java Bytecode Programs with Exceptions
2015 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, ISSN 1433-2779Article in journal (Refereed) Epub ahead of print
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.

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2015
Keywords
Software Verification, Static Analysis, Program Models
National Category
Computer Sciences
Research subject
Information and Communication Technology
Identifiers
urn:nbn:se:kth:diva-164580 (URN)10.1007/s10009-015-0375-0 (DOI)000385180700006 ()2-s2.0-84926377646 (Scopus ID)
Note

QP 2015

Available from: 2015-04-17 Created: 2015-04-17 Last updated: 2018-01-11Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-0074-8786

Search in DiVA

Show all publications