| 1. |
|
|
| 2. |
|
|
| 3. |
- Arts, Thomas, et al.
(författare)
-
Trace analysis of Erlang programs
- 2002. - 1
-
Konferensbidrag (refereegranskat)abstract
- The paper reports on an experiment to provide the Erlang programming language with a tool package for convenient trace generation, collection and to support analysis of traces using a set of techniques. Due to the frequent use of state-based software design patterns in Erlang programming we can in many cases recover not only the events from a trace log, but also the program states causing these events. This makes it possible to obtain program models from execution traces. In our work we make use of these program models for program visualization and model checking.
|
|
| 4. |
- Chugunov, Gennady, et al.
(författare)
-
Model checking of multi-applet JavaCard applications
- 2002. - 1
-
Konferensbidrag (refereegranskat)abstract
- The paper describes a framework for model checking JavaCard applets on the bytecode level. >From a set of JavaCard applets we extract their method call graphs using a static analysis tool. The resulting structure is translated into a pushdown system for which the model checking problem for Linear Temporal Logic (LTL) is decidable, and for which there are efficient model checking tools available. The model checking approach of the paper is tailored to the analysis of inter applet (intra card) communications and we demonstrate its effectiveness using a prototypical example of a purse applet and a set of loyalty applets.
|
|
| 5. |
|
|
| 6. |
|
|
| 7. |
|
|
| 8. |
- Dam, Mads, et al.
(författare)
-
On the Verification of Open Distributed Systems
- 1997. - 1
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- A logic and proof system is introduced for specifying and proving properties of open distributed systems. Key problems that are addressed include the verification of process networks with a changing interconnection structure, and where new processes can be continuously spawned. To demonstrate the results in a realistic setting we consider a core fragment of the Erlang programming language. Roughly this amounts to a first-order actor language with data types, buffered asynchronous communication, and dynamic process spawning. Our aim is to verify quite general properties of programs in this fragment. The specification logic extends the first-order $\mu$-calculus with Erlang-specific primitives. For verification we use an approach which combines local model checking with facilities for compositional verification. We give a specification and verification example based on a billing agent which controls and charges for user access to a given resource.
|
|
| 9. |
|
|
| 10. |
- Derrick, John, et al.
(författare)
-
Property-Based Testing - The ProTest Project
- 2010
-
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. ; 6286, s. 250-271
-
Tidskriftsartikel (refereegranskat)abstract
- The ProTest project is an FP7 STREP on property based testing. The purpose of the project is to develop software engineering approaches to improve reliability of service-oriented networks; support fault-finding and diagnosis based on specified properties of the system. And to do so we will build automated tools that will generate and run tests, monitor execution at run-time, and log events for analysis.The Erlang / Open Telecom Platform has been chosen as our initial implementation vehicle due to its robustness and reliability within the telecoms sector. It is noted for its success in the ATM telecoms switches by Ericsson, one of the project partners, as well as for multiple other uses such as in facebook, yahoo etc. In this paper we provide an overview of the project goals, as well as detailing initial progress in developing property based testing techniques and tools for the concurrent functional programming language Erlang.
|
|
