Opin vísindi

 

Nýlega bætt við

Verk
Tool Support for Holistic Modelling of Distributed Embedded Systems in Creol
(2009-07-28) Kyas, Marcel; Department of Computer Science
A holistic approach to modelling embedded systems is advocated: Many aspects of a system should be analysed in isolation to keep the task manageable, but they often influence each other during integration in a way that the desired system becomes unrealisable. A tool-supported approach that aims at integrated models of different concerns based on formal methods is suggested to solve this problem. This approach uses Creol, which is a language designed for object-oriented modelling of distributed systems. We report on ongoing work on the design and the implementation of tools that support modelling, validation, and verification. We focus on sensor networks, which are distributed system that consists of many embedded devices with tight constraints on computational power, energy availability, and timeliness. The described tools are a compiler that performs static checks and optimisations, an interpreter that defines a formal semantics, and a prototypical LTL model checker. This supports seamless development with formal methods.
Verk
Intra-Object versus Inter-Object : Concurrency and Reasoning in Creol
(2009-07-28) Johnsen, Einar Broch; Blanchette, Jasmin Christian; Kyas, Marcel; Owe, Olaf; Department of Computer Science
In thread-based object-oriented languages, synchronous method calls usually provide the mechanism to transfer control from caller to callee, blocking the caller until the call is completed. This model of control flow is well-suited for sequential and tightly coupled systems but may be criticized in the concurrent and distributed setting, not only for unnecessary delays but also for the reasoning complexity of multithreaded programs. Concurrent objects propose an alternative to multithread concurrency for object-oriented languages, in which each object encapsulates a thread of control and communication between objects is asynchronous. Creol is a formally defined modeling language for concurrent objects which clearly separates intra-object scheduling from inter-object communication by means of interface encapsulation, asynchronous method calls, and internal processor release points. This separation of concerns provides a very clean model of concurrency which significantly simplifies reasoning for highly parallel and distributed object-oriented systems. This paper gives an example-driven introduction to these basic features of Creol and discusses how this separation of concerns influences analysis of Creol models.
Verk
On message specifications in OCL
(2004-11-01) Kyas, Marcel; De Boer, Frank S.; Department of Computer Science
The object constraint language (OCL) is the established language for specifying of properties of objects and object structures. Recently an extension of OCL has been proposed for the specification of messages sent between objects. In this paper we present a generalization of this extension which allows additionally to specify causality constraints. From a pragmatic point of view, such causality constraints are needed to express, for example, that each acknowledgment must be preceded by a matching request, which is frequently required by communication protocols. Our generalization is based on the introduction of histories into OCL. Histories describe the external behavior of objects and groups of objects. Moreover, to reason compositionally about the behavior of a complex system we distinguish between local specifications of a single object and global specifications describing the interaction between objects. These two types of specifications are expressed in syntactically different dialects of OCL. Our notion of compositionality, which is formalized in this paper by a compatibility predicate on histories, allows the verification of models during the early stages of a design.
Verk
Iceland’s cruise infrastructure fee : Policy rationales, stakeholder tensions, and governance ambition
(2026-09) Hjálmarsdóttir, Hafdís Björg; Óskarsson, Guðmundur Kristján; Faculty of Business Administration
The rapid expansion of Arctic cruise tourism has intensified debates regarding sustainability, carrying capacity, and infrastructure pressure in vulnerable destinations. In response, the Icelandic government introduced an infrastructure fee on cruise ship passengers. This study examines how policymakers designed and justified the fee as a governance instrument, and what evidence would be required to establish that it functions as one. Using Iceland as a case study, the research combines qualitative document analysis of legislative and stakeholder materials with descriptive statistical data on cruise passenger flows. Policymakers framed the fee around infrastructure financing, the user-pays principle, fair contribution, and sustainable destination stewardship. However, the legislative process revealed stakeholder tensions concerning international competitiveness, regulatory predictability, and regional economic implications. Contextual data indicate a post-pandemic increase in passenger volumes relative to ship calls, highlighting the relevance of passenger-based indicators for understanding visitor intensity alongside vessel arrivals. The Icelandic case sits within a broader international trend, also visible in destinations such as Venice, Alaska, and Norway, in which authorities design and justify tourism taxation as a governance tool rather than solely as a revenue mechanism. The statutory framework does not earmark fee revenue for destination management, and an amendment adopted in 2025 reduced the rate with effect from 2026. The evidence examined establishes the fee’s governance objectives but does not demonstrate its destination-level effects.
Verk
Simplex-anchored regressors for fast global optimization-oriented miniaturization of microwave circuits
(2026-12) Koziel, Slawomir; Pietrenko-Dabrowska, Anna; Department of Engineering
The small physical size of high-frequency components is an essential prerequisite in an increasing number of applications. While size reduction of microwave circuits can be achieved with a suitable choice of architecture, ensuring the best available compromise between electrical parameters and size necessitates meticulous adjustment of all system dimensions. Due to the complexity of electrically small structures, parameter adjustment should be executed globally. Nevertheless, it is an expensive endeavor because it entails a large number of system evaluations executed through electromagnetic (EM) simulation. This article introduces an innovative approach to expedited miniaturization of microwave passives, in which the primary goal is miniaturization, while the conditions imposed on performance metrics are treated as constraints. Our framework operates in three stages, including parameter space pre-screening, machine-learning (ML)-driven globalized search, and gradient-based fine-tuning. The first stage involves random sampling aimed at identifying the most promising parameter space region. The ML process launched therein employs simplex-based regression models, the use of which contributes to a competitive computational efficiency. On the other hand, the final tuning improves design quality at a low cost, as it is realized as a local optimization process. The performance of the suggested algorithm is illustrated using two planar devices and demonstrated to be superior to several benchmark methods. The major advantages of our technique include low running costs, equivalent to only a few dozen full-wave analyses, and straightforward implementation.

Flokkar í Opnum vísindum

Veldu flokk til að skoða.

Niðurstöður 1 - 9 af 9