| 1. |
- Borgström, Johannes, et al.
(författare)
-
Broadcast Psi-calculi with an Application to Wireless Protocols
- 2011
-
Ingår i: Software Engineering and Formal Methods. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642246890 ; , s. 74-89
-
Konferensbidrag (refereegranskat)abstract
- Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. In this paper we add primitives for broadcast communication % to the psi-calculi framework. in order to model wireless protocols. The additions preserve the purity of the psi-calculi semantics, and we formally prove the standard congruence and structural properties of bisimilarity. We demonstrate the expressive power of broadcast psi-calculi by modelling the wireless ad-hoc routing protocol LUNAR and verifying a basic reachability property.
|
|
| 2. |
- Bubel, Richard, 1976, et al.
(författare)
-
A formalisation of Java Strings for program specification and verification
- 2011
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642246890 ; 7041, s. 90-105
-
Konferensbidrag (refereegranskat)abstract
- We present a formalisation of Java Strings tailored to specification and verification of programs (using dynamic logic). The formalism allows to specify and verify properties about the content of strings-the most common use-case-in an easy and natural manner. Each instance of type String is related to an abstract data type representing the string content as an immutable sequence of characters. This avoids serious technicalities that would arise if the specification had to resort to Java arrays to represent sequences of characters. We also discuss advanced aspects of Java Strings including string literals and the string pool and support for regular expressions. The approach has been implemented in the KeY verification system. We demonstrate its practical applicability by case studies including the verification of a string sanitization function.
|
|
| 3. |
- Noroozi, Neda, et al.
(författare)
-
Synchronizing Asynchronous Conformance Testing
- 2011
-
Ingår i: Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011). - Berlin : Springer Berlin/Heidelberg. - 9783642246890 ; , s. 334-349
-
Konferensbidrag (refereegranskat)abstract
- We present several theorems and their proofs which enable using synchronous testing techniques such as input output conformance testing (ioco ) in order to test implementations only accessible through asynchronous communication channels. These theorems define when the synchronous test-cases are sufficient for checking all aspects of conformance that are observable by asynchronous interaction with the implementation under test. © 2011 Springer-Verlag.
|
|
| 4. |
- Soleimanifard, Siavash, et al.
(författare)
-
ProMoVer : Modular Verification of Temporal Safety Properties
- 2011
-
Ingår i: Software Engineering and Formal Methods (SEFM) 2011. - Berlin, Heidelberg : Springer. - 9783642246890 ; , s. 366-381
-
Konferensbidrag (refereegranskat)abstract
- This paper describes ProMoVer, a tool for fully automated procedure–modular verification of Java programs equipped with method–local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure–level is a natural instantiation of the modular verification paradigm, where correctness ofglobal properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositionalverification of control flow safety properties, and provides appropriatepre– and post–processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verfication tasks resulting from changes in the code and the specifications. The verification task is relatively light–weight due to support for abstraction from private methods and automatic extraction of candidate specifications from methodimplementations. We evaluate the tool on a number of applications from the smart card domain.
|
|
