| 1. |
- de C. Gomes, Pedro, et al.
(author)
-
Specification and verification of synchronization with condition variables
- 2018
-
In: Science of Computer Programming. - : Elsevier. - 0167-6423 .- 1872-7964. ; 163, s. 174-189
-
Journal article (peer-reviewed)abstract
- 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.
|
|
| 2. |
- Felderer, Michael, 1978-, et al.
(author)
-
Formal methods in industrial practice - Bridging the gap (track summary)
- 2018
-
In: Lect. Notes Comput. Sci.. - Cham : Springer Verlag. - 9783030034269 ; , s. 77-81
-
Conference paper (peer-reviewed)abstract
- 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).
|
|
| 3. |
- Gurov, Dilian, 1964-, et al.
(author)
-
A Hoare Logic Contract Theory : An Exercise in Denotational Semantics
- 2018
-
In: Principled Software Development. - Cham : Springer Nature. ; , s. 119-127
-
Book chapter (other academic/artistic)abstract
- We sketch a simple theory of Hoare logic contracts for programs with procedures, presented in denotational semantics. In particular, we give a simple semantic justification of the usual procedure-modular treatment of such programs. The justification is given by means of a proof of soundness of a contract-relative denotational semantics against the standard denotational semantics of procedures in the context of procedure declarations. The suggested formal development can be used as an inspiration for more ambitious contract theories.
|
|
| 4. |
- Nyberg, Mattias, et al.
(author)
-
Formal verification in automotive industry : Enablers and obstacles
- 2018
-
In: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018. - Cham : Springer. - 9783030034269 ; , s. 139-158
-
Conference paper (peer-reviewed)abstract
- 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.
|
|
