Change search
Link to record
Permanent link

Direct link
BETA
Publications (5 of 5) Show all publications
Artho, C. & Ölveczky, P. (2019). Formal Techniques for Safety-Critical Systems (FTSCS 2016). Science of Computer Programming, 175, 35-36
Open this publication in new window or tab >>Formal Techniques for Safety-Critical Systems (FTSCS 2016)
2019 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 175, p. 35-36Article in journal, Editorial material (Refereed) Published
Place, publisher, year, edition, pages
Elsevier, 2019
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-246449 (URN)10.1016/j.scico.2019.02.001 (DOI)000462421700003 ()2-s2.0-85061666421 (Scopus ID)
Note

QC 20190329

Available from: 2019-03-29 Created: 2019-03-29 Last updated: 2019-04-26Bibliographically approved
Artho, C. & Visser, W. (2019). Java Pathfinder at SV-COMP 2019 (Competition Contribution). In: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019: . Paper presented at 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019; Prague; Czech Republic; 6 April 2019 through 11 April 2019 (pp. 224-228). Springer, 11429
Open this publication in new window or tab >>Java Pathfinder at SV-COMP 2019 (Competition Contribution)
2019 (English)In: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Springer, 2019, Vol. 11429, p. 224-228Conference paper, Published paper (Refereed)
Abstract [en]

This paper gives a brief overview of Java Pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.

Place, publisher, year, edition, pages
Springer, 2019
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 11429
Keywords
Java Pathfinder, Java program analysis, Software model checking
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-251826 (URN)10.1007/978-3-030-17502-3_18 (DOI)2-s2.0-85064939176 (Scopus ID)9783030175016 (ISBN)
Conference
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019; Prague; Czech Republic; 6 April 2019 through 11 April 2019
Note

QC 29190523

Available from: 2019-05-23 Created: 2019-05-23 Last updated: 2019-05-23Bibliographically approved
Artho, C. & Ölveczky, P. (2018). Formal Techniques for Safety-Critical Systems (FTSCS 2015). Science of Computer Programming, 154, 1-2
Open this publication in new window or tab >>Formal Techniques for Safety-Critical Systems (FTSCS 2015)
2018 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 154, p. 1-2Article in journal (Refereed) Published
Place, publisher, year, edition, pages
Elsevier B.V., 2018
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:kth:diva-223125 (URN)10.1016/j.scico.2017.12.008 (DOI)000425077800001 ()2-s2.0-85039154257 (Scopus ID)
Note

Export Date: 13 February 2018; Editorial; CODEN: SCPGD. QC 20180327

Available from: 2018-03-27 Created: 2018-03-27 Last updated: 2018-03-27Bibliographically approved
Kitamura, T., Maissonneuve, Q., Choi, E.-H. -., Artho, C. & Gargantini, A. (2018). Optimal Test Suite Generation for Modified Condition Decision Coverage Using SAT Solving. In: 37th International Conference on Computer Safety, Reliability and Security, SAFECOMP 2018: . Paper presented at 18 September 2018 through 21 September 2018 (pp. 123-138). Springer
Open this publication in new window or tab >>Optimal Test Suite Generation for Modified Condition Decision Coverage Using SAT Solving
Show others...
2018 (English)In: 37th International Conference on Computer Safety, Reliability and Security, SAFECOMP 2018, Springer, 2018, p. 123-138Conference paper, Published paper (Refereed)
Abstract [en]

Boolean expressions occur frequently in descriptions of computer systems, but they tend to be complex and error-prone in complex systems. The modified condition decision coverage (MCDC) criterion in system testing is an important testing technique for Boolean expression, as its usage mandated by safety standards such as DO-178 [1] (avionics) and ISO26262 [2] (automotive). In this paper, we develop an algorithm to generate optimal MCDC test suites for Boolean expressions. Our algorithm is based on SAT solving and generates minimal MCDC test suites. Experiments on a real-world avionics system confirm that the technique can construct minimal MCDC test suites within reasonable times, and improves significantly upon prior techniques.

Place, publisher, year, edition, pages
Springer, 2018
Keywords
Avionics, Fighter aircraft, Network security, Avionics systems, Boolean expressions, Error prones, Modified condition decision coverage, Safety standard, SAT-solving, System testing, Testing technique, Safety testing
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-236369 (URN)10.1007/978-3-319-99130-6_9 (DOI)000458564600009 ()2-s2.0-85053750350 (Scopus ID)9783319991290 (ISBN)
Conference
18 September 2018 through 21 September 2018
Note

QC 20181105

Available from: 2018-11-05 Created: 2018-11-05 Last updated: 2019-03-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
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-3656-1614

Search in DiVA

Show all publications