| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Using Forward Reachability Analysis for Verification of Timed Petri Nets
- 2007
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 14:1, s. 1-42
-
Tidskriftsartikel (refereegranskat)abstract
- We consider verification of safety properties for concurrent real-timed systems modelled as timed Petri nets by performing symbolic forward reachability analysis. We introduce a formalism, called region generators, for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions and provide exact abstractions of sets of reachable states with respect to safety properties. We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples. We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer's protocol, Lynch and Shavit's mutual exclusion protocol and a producer-consumer protocol. We also used the tool to extract finite-state abstractions of these protocols.
|
|
| 2. |
- Amnell, Tobias, et al.
(författare)
-
Code Synthesis for Timed Automata
- 2002
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 9:4, s. 269-300
-
Tidskriftsartikel (refereegranskat)
|
|
| 3. |
|
|
| 4. |
|
|
| 5. |
|
|
| 6. |
- Bosch, Jan
(författare)
-
Delegating Compiler Objects : Modularity and Resuability in Language Engineering
- 1997
-
Ingår i: Nordic Journal of Computing. - Helsinki : Nordic Journal of Computing. - 1236-6064. ; 4:1, s. 66-92
-
Tidskriftsartikel (refereegranskat)abstract
- The application domain of compiler techniques is changing. Whereas previously compiler techniques were primarily used for the construction of compilers for general-purpose languages, now these techniques are increasingly often used for the construction of application domain languages and extensible language models. However, the traditional compiler techniques suffer from problems of complexity, maintainability, reusability and extensibility, and new approaches are needed. In this paper, we describe the notion of delegating compiler objects (DCOs), a novel approach to compiler construction that provides structural decomposition and reusability of compiler specifications. Our extensible language, the layered object model, is used to illustrate the advantages of the DCO approach for compiler construction.
|
|
| 7. |
|
|
| 8. |
|
|
| 9. |
- Hammar, Mikael, et al.
(författare)
-
Improved Exploration of Rectilinear Polygons
- 2002
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 9:1, s. 32-53
-
Tidskriftsartikel (refereegranskat)abstract
- We prove a 5/3-competitive strategy for exploring a simple rectilinear polygon in the $L_1$ metric. This improves the previous factor two bound of Deng, Kameda and Papadimitriou.
|
|
| 10. |
- Jonsson B, Margaria T, Naeser G, Nyström J, Steffen B
(författare)
-
Incremental Requirement Specification for Evolving Systems
- 2001
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 8:1, s. 65-87
-
Tidskriftsartikel (refereegranskat)abstract
- We propose a technique for hierarchically structuring requirement specifications in a way that simplifies change management. Our technique decomposes the process of requirement specification and validation. Specifications, added or modified incrementally
|
|
| 11. |
- Lind, Kenneth, 1966, et al.
(författare)
-
Estimation of Real-Time Software Component Size
- 2008
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 14, s. 282-300
-
Tidskriftsartikel (refereegranskat)abstract
- For distributed networks which will be mass-produced, such as computer systems in modern vehicles, it is crucial to develop cost-efficient hardware. A distributed network in a vehicle can consist of 100 ECUs (Electronic Control Unit). In this paper we consider the amount of memory needed for these ECUs. They should contain enough memory to survive several software generations, without inducing unnecessary cost of too much memory. We show that UML Component Diagrams can be used to collect enough information for estimating memory size using an FSM method. We develop two linear models capable of estimating memory size for two common types of software components before the software is available. We support our findings by two experiments containing several software components from the automotive industry.
|
|
| 12. |
- Lundberg, Lars, et al.
(författare)
-
Bounding the gain of changing the number of memory modules in shared memory multiprocessors
- 1997
-
Ingår i: Nordic Journal of Computing. - Finland : Publishing Assoc. Nordic Journal of Comput. - 1236-6064. ; 4:3, s. 233-58
-
Tidskriftsartikel (refereegranskat)abstract
- We consider a multiprocessor, with p processors and m memory modules. If more than one processor want to access a memory module simultaneously, these accesses will be serialized due to memory contention. The completion time of a program executing on this system is thus affected by the way addresses are mapped onto memory modules, and finding a mapping which results in minimal completion time is NP-hard. If we change the number of memory modules from m to m’, while keeping the number processors constant, we will generally change the minimal completion time. The gain of changing the number of memory modules from m to m’ for a certain program is defined as the ratio between the minimal completion times, using m and m’ modules respectively. Here, we present an optimal upper bound on the maximum gain of changing the number of memory modules, as a function of m, m’ and p, including the case when m’ is infinitely large. The bound is obtained by investigating a mathematical formulation. The mathematical tools involved are essentially elementary combinatorics. The formula for calculating the bound is mathematically complicated but can be rapidly computed for reasonable m, m’ and p. This bound makes it possible to do price-performance trade-offs and to compare any mapping of addresses to memory modules with the optimal case. The results are applicable to different multiprocessor architectures, e.g. systems with crossbar networks and systems with multiple buses. The results also make it possible to calculate optimal performance bounds for multiprocessors containing cache memories: as well as for multiprocessors with no cache memories. Moreover, we discuss how the results can be used for calculating bounds for programs with as well as without synchronizations.
|
|
| 13. |
- Magnusson, Eva, et al.
(författare)
-
Program Visualization using Reference Attributed Grammars
- 2000
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 7, s. 67-86, s. 76-96
-
Tidskriftsartikel (refereegranskat)abstract
- This paper describes how attribute grammars can be used to integrate program visualization in language-based environments and how program visualizations can be specified and generated from grammars. It is discussed how a general solution for a simple grammar can be reused in grammars for other specific languages. As an example we show how diagram generation for a very simple state transition language can be integrated in a more complex specific state transition language. We use an extended form of attribute grammars, RAGs, which permits attributes to be references to nodes in the syntax tree. An external graph drawing tool is used to visualize the diagrams. The solution is modularized to support reuse for different languages and exchange of the external drawing tool for different types of visualization.
|
|
| 14. |
- Mousavi, Mohammad Reza, 1978-, et al.
(författare)
-
Timed-Gamma and Its Coordination Language
- 2015
-
Ingår i: Nordic Journal of Computing. - Helsinki : University of Helsinki. - 1236-6064. ; 15:2, s. 75-111
-
Tidskriftsartikel (refereegranskat)abstract
- This paper proposes a theoretical framework for separation of concerns in the formal specification of reactive and real-time systems. This framework consists of the syntax and the semantics of three languages (and all meaningful combinations thereof) that each address a separate concern. The first language, Gamma (a variant of an existing language) is used to define the functionality of a system (by means of a set of basic data transformations). Our additions are a simple language of intervals specifying timing-properties of basic transformations and a language (called Schedules) for specifying the coordination of the basic Gamma transformations. Each of these languages formally models a separate aspect of a system and statements in these languages can be reused, changed or analyzed in their own right. Our key contribution is that we provide a formal framework in which different combinations of aspects have a well-defined semantics.
|
|
| 15. |
- Nilsson, Anders, et al.
(författare)
-
Implementing Java Compilers Using ReRAGs
- 2004
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 11:3, s. 213-234
-
Tidskriftsartikel (refereegranskat)abstract
- Rewritable Reference Attributed Grammars (ReRAGs) is a recently developed compiler-compiler technology based on object-orientation, aspect-orientation, reference attributed grammars, and conditional rewrites. In this paper we describe our experiences from using ReRAGs for implementing Java compilers. We illustrate how the usage of ReRAGs renders a rather compact, yet easy-to-understand and modular compiler specification where code analysis, restructurings, and optimizations can be conveniently described as aspects performing computations and transformations on the abstract syntax tree. Currently, we have implemented two compilers: one that generates C code with real-time support, and one that generates Java bytecode. Both share the same front end.
|
|
| 16. |
- Parrow, Joachim
(författare)
-
Interaction Diagrams
- 1995
-
Ingår i: Nordic Journal of Computing. - 1236-6064. ; 2:4, s. 407-443
-
Tidskriftsartikel (refereegranskat)
|
|
| 17. |
- Pettersson, Cecilia, 1963, et al.
(författare)
-
Debate: Study Protocol: The Physical Environment and Home Healthcare Services: The Development and Content of A Study Protocol to Explore Enablers and Barriers in the Physical Environment for the Delivery of Home Healthcare Services
- 2019
-
Ingår i: Nordisk arkitekturforskning. - : SINTEF Academic Press. - 1893-5281 .- 1102-5824 .- 1236-6064. ; 31:2, s. 105-122
-
Tidskriftsartikel (refereegranskat)abstract
- Whilst home healthcare services for an aging population currently living in ordinary housing are increasingly needed, physical environments do not adequately meet current levels of demand for such services. The present study protocol, which combines qualitative and quantitative methods, was developed in order to explore the impact of architectural design on enablers and barriers in the delivery of home healthcare services. An interdisciplinary research team, drawn from the fields of architecture, healthcare, and occupational sciences, will execute the forthcoming study. This study protocol describes the design of that study, which will explore the relation between residential design and the conditions for care in ordinary housing.
|
|
