The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
The motivation behind pattern-oriented software development is to decompose complex problems into recognizable sub-problems with predefined solutions, hence promoting both the quality of the resulting software product and the efficiency of the development process through the reuse of optimal solutions (e.g., best practices). Unfortunately, due to the opportunistic (i.e., non-systematic and subjective)...
The modernization of a software system is a complex and expensive task and requires a deep understanding of the existing system. The capability of re-factoring a complex application into some high-level views is mandatory to elicit its structure and start localize possible changes. The high number of different implementation technologies imposes a model-based, neutral approach to reconstruct the structure...
Interrupt behaviors are extremely difficult to verify and reason about in the development of operating system due to their randomicity and nondeterminism. This paper proposes a formal model of interrupt program which is an extension of Dijkstra's language of guarded commands. The probabilistic operational semantics exhibiting how the effect of interrupt is produced is explored for the interrupt program...
One pillar of Model-Driven Development for real-time embedded software is the separation of concerns between application model and target platform. This requires definition of model transformations realizing the mapping of the application model onto the target platform. Real-Time and Embedded Systems design means coping with different target platforms and with heterogeneous constraints related to...
The INESS (Integrated European Signalling System) Project, funded by the FP7 programme of the European Union, aims to provide a common, integrated, railway signalling system within Europe. INESS experts have been using the Executable UML (xUML) language to model an executable specification of the proposed system. Due to safety-critical aspects of these systems, one key idea is to formally analyse...
Designing and developing mission-critical embedded systems is challenging, especially due to additional platform constraints regarding timing and computational resources. The development process of embedded systems should include verification techniques already at the architecture design phase, to provide evidence that a system's architecture fulfills its requirements. The Architecture Analysis and...
Several approaches adopted by the software engineering community rely on the principle of multi-modeling which allows to separate concerns and to model a system as a set of less complex sub-models. Model composition is a crucial activity in Model Driven Engineering (MDE). It is particularly useful when adopting a multi-modeling approach to analyze and design software systems. In previous work, we...
With most of formal methods, an initial formal model can be refined in multiple steps, until the final refinement contains enough details for an implementation. Most of the time, this initial model is built from the description obtained by the requirements analysis. Unfortunately, this transition from the requirements phase to the formal specification phase is one of the most painful steps and is...
The specifications of the control units driving embedded systems often involve temporal properties. We aim at certifying them statically using the Abstract Interpretation framework and introduce several Abstract Domains dedicated to proving such temporal properties. This work defines the specificity of such domains, that we call Temporal Abstract Domains. We introduce a continuous-time abstraction,...
Construction of a Real-Time System (RTS) out of a number of pre-fabricated pieces of software, otherwise known as components, is a pervasive area of interest. Typically, only relocatable object code of the component is shipped to the customer, so that it can later be linked into the overall application. Source code is therefore withheld, and disassembling of the object code is normally disallowed...
AADL is a modeling language to design and analyze High-Integrity Distributed and Real-time systems. Embedded sub-languages published as AADL annexes extend an AADL model to enhance analysis. The behavior annex specifies the behavior of an AADL application model. Thus, an implantation of this annex allows to perform behavior analysis. In addition, as there are several AADL annexes, the implementation...
Wireless sensor networks consist of resource constrained nodes, especially with respect to power resources. In many cases, the replacement of a dead node is difficult and costly, e.g. an implanted node in the human body. Our main goal in this paper is reducing the total power consumption of the network. For this purpose, we consider the cooperation of nodes in data transmission in terms of a group,...
In this paper, we present different modeling and execution frameworks that allow us to efficiently analyze, design and verify complex systems, mainly to cope with the specific concerns of the Real-time and embedded systems (RTE) domain. First we depict a UML /MARTE based methodology for executable RTE systems modeling with a framework and its underlying model transformations required to execute UML...
This paper presents a methodology for generating a web service "stub" that simulates the behaviour of a real-world SOAP web service. The simulation is driven by a formal description of the original service's input and output parameters, messages, and ordering constraints between messages, using an extension of Linear Temporal Logic called LTL-FO+. This logic is rich enough to express complex...
The reverse engineering of behavioral models consists in extracting high-level models that help understand the behavior of existing software systems. In the context of reverse engineering of sequence diagrams, most approaches strongly depend on the static analysis and instrumentation of the source code to produce correct diagrams that take into account control flow structures such as alternative blocks...
In this paper, we show that both global as well as local schedulability analysis of synchronization protocols based on the stack resource policy (SRP) and overrun without payback for hierarchical scheduling frameworks based on fixed-priority preemptive scheduling (FPPS) are pessimistic. We present tighter global and local schedulability analysis, illustrate the improvements of the new analysis by...
The Clock Constraint Specification Language (CCSL) provides expressions and relations to specify the time requirements and causal dependencies of systems. It was initially proposed, in the context of MARTE: the UML profile for Modeling and Analysis of Real-Time and Embedded Systems. In this paper, we propose a method to verify CCSL specifications. We give a formal state-based interpretation of a fundamental...
The process of determining the worst-case execution time (WCET) is challenged in the presence of caches due to their unpredictable effect on the speed of memory references. In particular, when cache conflicts between program lines are common, thrashing occurs and this inadvertently increases the WCET, sometimes significantly so. One way to minimise the cache impact on the WCET, therefore, is to judiciously...
The documentation of customer needs from the source specifications in a modeling environment for allocating them to architectural elements needs efficient tools and techniques in requirement engineering. Once requirements are present in models, enhancement with suitable properties, classification, prioritization. and allocation on system architecture are then possible. A downside is that the customer...
The paper presents a case study of building solution for automation of Integrated Modular Avionics system design and system integration processes within existing industrial environment on base of model driven approaches. Features of modern architecture description language are discussed and experience of building a tool chain on top of one of them is described.
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.