Change search
Link to record
Permanent link

Direct link
BETA
Publications (10 of 40) Show all publications
Felderer, M., Gurov, D., Huisman, M., Lisper, B. & Schlick, R. (2018). Formal methods in industrial practice - Bridging the gap (track summary). In: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018: . Paper presented at 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018; Limassol; Cyprus; 5 November 2018 through 9 November 2018 (pp. 77-81). Springer, 11247
Open this publication in new window or tab >>Formal methods in industrial practice - Bridging the gap (track summary)
Show others...
2018 (English)In: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018, Springer, 2018, Vol. 11247, p. 77-81Conference paper, Published paper (Refereed)
Abstract [en]

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

Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 11247
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-246544 (URN)10.1007/978-3-030-03427-6_10 (DOI)2-s2.0-85056479295 (Scopus ID)9783030034269 (ISBN)
Conference
8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018; Limassol; Cyprus; 5 November 2018 through 9 November 2018
Note

QC 20190328

Available from: 2019-03-28 Created: 2019-03-28 Last updated: 2019-03-28Bibliographically approved
Nyberg, M., Gurov, D., Lidström, C., Rasmusson, A. & Westman, J. (2018). Formal verification in automotive industry: Enablers and obstacles. In: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018: . Paper presented at 5 November 2018 through 9 November 2018 (pp. 139-158). Springer Verlag
Open this publication in new window or tab >>Formal verification in automotive industry: Enablers and obstacles
Show others...
2018 (English)In: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018, Springer Verlag , 2018, p. 139-158Conference paper, Published paper (Refereed)
Abstract [en]

We describe and summarize our experiences from six industrial case studies in applying formal verification techniques to embedded, safety-critical code. The studies were conducted at Scania over the period of eight years. Despite certain successes, we have so far failed to introduce formal techniques on a larger scale. Based on our experiences, we identify and discuss some key obstacles to, and enabling factors for the successful incorporation of formal verification techniques into the software development and quality assurance process. 

Place, publisher, year, edition, pages
Springer Verlag, 2018
Keywords
Accident prevention, Automotive industry, Quality assurance, Software design, Critical codes, Formal techniques, Industrial case study, Quality assurance process, Verification techniques, Formal verification
National Category
Software Engineering
Identifiers
urn:nbn:se:kth:diva-247483 (URN)10.1007/978-3-030-03427-6_14 (DOI)2-s2.0-85056454420 (Scopus ID)9783030034269 (ISBN)
Conference
5 November 2018 through 9 November 2018
Note

QC20190405

Available from: 2019-04-05 Created: 2019-04-05 Last updated: 2019-04-05Bibliographically approved
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
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-0074-8786

Search in DiVA

Show all publications