| 1. |
- Bubel, Richard, 1976, et al.
(författare)
-
Integration of Informal and Formal Development of Object-Oriented Safety-Critical Software: A Case Study with the KeY System
- 2003
-
Ingår i: Electronic Notes in Theoretical Computer Science. - 1571-0661. ; 80, s. 3-25
-
Konferensbidrag (refereegranskat)abstract
- The KeY system allows integrated informal and formal development of objectoriented Java software. In this paper we report on a major industrial case study involving safety-critical software for computation of a particular kind of railway time table used by train drivers. Our case study includes formal specification of requirements on the analysis and the implementation level. Particular emphasis in our research is put on the challenge of how authoring and maintenance of formal specifications can be made easier. We demonstrate that the technique of specification patterns implemented in KeY for the language OCL yields significant improvements.
|
|
| 2. |
- Een, Niklas, 1973, et al.
(författare)
-
Temporal Induction by Incremental SAT Solving
- 2003
-
Ingår i: Electronical Notes in Theoretical Computer Science. - 1571-0661. ; 89:4, s. 543-560
-
Tidskriftsartikel (refereegranskat)abstract
- We show how a very modest modification to a typical modern SAT-solver enables it to solve a series of related SAT-instances efficiently. We apply this idea to checking safety properties by means of temporal induction, a technique strongly related to bounded model checking. We further give a more efficient way of constraining the extended induction hypothesis to so called loop-free paths. We have also performed the first comprehensive experimental evaluation of induction methods for safety-checking.
|
|
| 3. |
- Magnusson, Eva, et al.
(författare)
-
Circular Reference Attributed Grammars - their Evaluation and Applications
- 2003
-
Ingår i: ENTCS - Electronic Notes in Computer Science. - 1571-0661. ; 82:3, s. 532-554
-
Konferensbidrag (refereegranskat)abstract
- This paper presents a combination of Reference Attributed Grammars (RAGs) and Circular Attribute Grammars (CAGs). While RAGs allow the direct and easy specification of non-locally dependent information, CAGs allow iterative fixed-point computations to be expressed directly using recursive (circular) equations. We demonstrate how the combined formalism, Circular Reference Attributed Grammars (CRAGs), can take advantage of both these strengths, making it possible to express solutions to many problems in an easy way. We exemplify with the specification and computation of the nullable, first, and follow sets used in parser construction, a problem which is highly recursive and normally programmed by hand using an iterative algorithm. We also present a general demand-driven evaluation algorithm for CRAGs and some optimizations of it. The approach has been implemented and experimental results include computations on a series of grammars including Java 1.2. We also revisit some of the classical examples of CAGs and show how their solutions are facilitated by CRAGs.
|
|
| 4. |
- Angelsmark, Ola, 1972-
(författare)
-
Constraints, Adjunctions and (Co)algebras
- 2000
-
Ingår i: Coalgebraic Methods in Computer Science CMCS-2000,2000. - : Science Direct. ; 33
-
Konferensbidrag (refereegranskat)abstract
- The connection between constraints and universal algebra has been looked at in, e.g Jeavons, Cohen and Pearson, 1998, and has given interesting results. Since the connection between universal algebra and category theory is so obvious, we will in this paper investigate if the usage of category theory has any impact on the results and/or reasoning and if anything can be gained from this approach. We construct categories of problem instances and of solutions to these, and, via an adjunction between these categories, note that the algebras give us a way of describing 'minimality of a problem,' while the coalgebras give a criterion for deciding if a given set of solutions can be expressed by a constraint problem of a given arity. Another pair of categories, of sets of relations and of sets of operations on a fixed set, is defined, and this time the algebras we get give an indication of the 'expressive power' of a set of constraint types, while the coalgebras tell us about the computational complexity of the corresponding constraint problem.
|
|
| 5. |
- Assmann, Uwe
(författare)
-
Automatic Roundtrip Engineering
- 2003
-
Ingår i: Electronic Notes in Theoretical Computer Science. - 1571-0661. ; 82:5, s. 33-41
-
Tidskriftsartikel (övrigt vetenskapligt/konstnärligt)abstract
- A systematic method for roundtrip engineering of systems, automatic roundtrip engineering (ARE), is presented. It relies on the automatic derivation of inverses for domain transformations. While roundtrip engineering is a well known system engineering method, systematic conditions for its deployment have not yet been formalized, and this is done in the paper. Secondly, ARE is a generic architectural style for different architectural scenarios. To show this, the paper gives a first classification, defining several subclasses of ARE systems: sequenced ARE systems, automatic Model-View-Controller engineering (MVARE), and bidirectional aspect systems (Beavers). Sequenced ARE systems extend the ARE principle to chains of transformations. MVARE systems project a domain into a set of simpler ones, simplifying system understanding. Beaving systems generalize aspect-oriented programming to roundtrip engineering. All ARE classes describe different generic application architectures and have a great potential to simplify the construction of roundtrip engineering tools and applications.
|
|
| 6. |
- Dell'Acqua, Pierangelo, 1963-, et al.
(författare)
-
A logic based asynchronous multi-agent system
- 2002
-
Ingår i: Electronical Notes in Theoretical Computer Science. - 1571-0661 .- 1571-0661. ; 70:5, s. 72-88
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- We present a logic programming based asynchronous multi-agent system in which agents can communicate with one another, update themselves and each other, abduce hypotheses to explain observations, and use them to generate actions. The knowledge base of the agents is comprised of generalized logic programs, integrity constraints, active rules, and of abducibles. We characterize the interaction among agents via an asynchronous transition rule system, and provide a stable models based semantics. An example is developed to illustrate how our approach works. © 2002 Published by Elsevier Science B.V.
|
|
| 7. |
- Drabent, Wlodek, et al.
(författare)
-
Type-based diagnosis of CLP programs
- 2000
-
Ingår i: WLPE'99. - Amsterdam : Elsevier. ; 30:4, s. 215-234
-
Konferensbidrag (refereegranskat)abstract
- The paper presents a diagnosis tool for CLP programs. It deals with partial correctness w.r.t. specifications which describe procedure calls and successes. The space of possible specifications is restricted to a kind of regular types; we propose a generalization of the concept of types used in so called descriptive typing of logic programs. In particular we distinguish ground types from those containing non-ground elements.The tool is able to automatically locate at compile time all errors in a program, this means all the clauses or clause prefixes responsible for the program being incorrect w.r.t. a given specification. The tool aids the user in constructing specifications incrementally; often a fragment of the specification is already sufficient to locate an error.Our prototype is specialized for the programming language CHIP, but the idea is applicable to any untyped CLP (and LP) language. We believe that the presented approach makes it possible to combine the advantages of typed and untyped programming languages.
|
|
| 8. |
- Eklund, Patrik, 1958-, et al.
(författare)
-
A categorical approach to unication of generalised terms
- 2002
-
Ingår i: Electronic Notes in Theoretical Computer Science. - : Elsevier. - 1571-0661. ; 66:5, s. 41-45
-
Tidskriftsartikel (refereegranskat)abstract
- Unification of generalised terms in a many-valued setting involves considerations for equalities in the sense of similarity degrees between operators and thus similarities between terms. Further, allowing for substitutions of variables with powersets of terms requires ‘flattening’ operators for handling composition of variable substitutions. These techniques are available when using powerset functors composed with the term functor so that this composition of functors is extendable to a monad. In this paper we provide a framework for unification of such generalised terms.
|
|
| 9. |
- Eklund, Patrik, 1958-, et al.
(författare)
-
A graphical approach to monad composition
- 2001
-
Ingår i: Electronic Notes in Theoretical Computer Science. - 1571-0661. ; 40, s. 145-160
-
Tidskriftsartikel (refereegranskat)abstract
- In this paper we show how composite expressions involving natural transformations can be pictorially represented in order to provide graphical proof support for providing monad compositions. Examples are drawn using powerset monads composed with the term monad.
|
|
| 10. |
- Hammarberg, Jerker, et al.
(författare)
-
Development of safety-critical reconfigurable hardware with esterel
- 2003
-
Ingår i: Electronic Notes in Theoretical Computer Science. - 1571-0661. ; 80, s. 229-244
-
Konferensbidrag (övrigt vetenskapligt/konstnärligt)abstract
- Demands for higher flexibility in aerospace applications has led to increasing deployment of FPGAs. Clearly, analysis of safety-related properties of such components is essential for their use in safety-critical subsystems. The contributions of this paper are twofold. First, we illustrate a development process, using a language with formal semantics (Esterel) for design, formal verification of high-level design and automatic code generation down to VHDL. We argue that this process reduces the likelihood of systematic (permanent) faults in the design, and still produces VHDL code that is of acceptable quality (size of FPGA, delay). Secondly, we show how the design model can be modularly extended with fault models that represent random faults (e.g. radiation) leading to bit flips in the component under design (resembling FMEA), and transient or permanent faults in the rest of the environment (corrupting inputs to the component or jeopardising the effect of output signals that control the environment). The set-up is then used to formally determine which (single or multiple) fault modes cause violation of the top-level safety-related property, much in the spirit of fault-tree analyses. An aerospace hydraulic monitoring system is used to illustrate the results. © 2003 Published by Elsevier Science B.V.
|
|
