Timing analysis of assembler code control-flow paths

Timinganalysis of assembler code is essential to achieve the strongest possible guarantee of correctness for safety-critical, real-time software. Previous work has shown how timingconstrain ts on controlflow paths through high-level language programs can be formalised using the semantics of the statements comprisingthe path. We extend these results to assembler-level code where it becomes possible to not only determine timingconstrain ts, but also to verify them against the known execution times for each instruction. A minimal formal model is developed with both a weakest liberal precondition and a strongest postcondition semantics. However, despite the formalism’s simplicity, it is shown that complex timingb ehaviour associated with instruction pipeliningand iterative code can be modelled accurately.

A partial-correctness semantics for modelling assembler programs

Previous work on formally modelling and analysing program compilation has shown the need for a simple and expressive semantics for assembler level programs. Assembler programs contain unstructured jumps and previous formalisms have modelled these by using continuations, or by embedding the program in an explicit emulator. We propose a simpler approach, which uses techniques from compiler theory in a formal setting. This approach is based on an interpretation of programs as collections of program paths, each of which has a weakest liberal precondition semantics. We then demonstrate, by example, how we can use this formalism to justify the compilation of block-structured high-level language programs into assembler.

The development of hard real-time systems using a formal approach

Hard real-time systems are a class of computer control systems that must react to demands of their environment by providing `correct' and timely responses. Since these systems are increasingly being used in systems with safety implications, it is crucial that they are designed and developed to operate in a correct manner. This thesis is concerned with developing formal techniques that allow the specification, verification and design of hard real-time systems. Formal techniques for hard real-time systems must be capable of capturing the system's functional and performance requirements, and previous work has proposed a number of techniques which range from the mathematically intensive to those with some mathematical content. This thesis develops formal techniques that contain both an informal and a formal component because it is considered that the informality provides ease of understanding and the formality allows precise specification and verification. Specifically, the combination of Petri nets and temporal logic is considered for the specification and verification of hard real-time systems. Approaches that combine Petri nets and temporal logic by allowing a consistent translation between each formalism are examined. Previously, such techniques have been applied to the formal analysis of concurrent systems. This thesis adapts these techniques for use in the modelling, design and formal analysis of hard real-time systems. The techniques are applied to the problem of specifying a controller for a high-speed manufacturing system. It is shown that they can be used to prove liveness and safety properties, including qualitative aspects of system performance. The problem of verifying quantitative real-time properties is addressed by developing a further technique which combines the formalisms of timed Petri nets and real-time temporal logic. A unifying feature of these techniques is the common temporal description of the Petri net. A common problem with Petri net based techniques is the complexity problems associated with generating the reachability graph. This thesis addresses this problem by using concurrency sets to generate a partial reachability graph pertaining to a particular state. These sets also allows each state to be checked for the presence of inconsistencies and hazards. The problem of designing a controller for the high-speed manufacturing system is also considered. The approach adopted mvolves the use of a model-based controller: This type of controller uses the Petri net models developed, thus preservIng the properties already proven of the controller. It. also contains a model of the physical system which is synchronised to the real application to provide timely responses. The various way of forming the synchronization between these processes is considered and the resulting nets are analysed using concurrency sets.

Development of real-time process control systems using formal techniques

A major application of computers has been to control physical processes in which the computer is embedded within some large physical process and is required to control concurrent physical processes. The main difficulty with these systems is their event-driven characteristics, which complicate their modelling and analysis. Although a number of researchers in the process system community have approached the problems of modelling and analysis of such systems, there is still a lack of standardised software development formalisms for the system (controller) development, particular at early stage of the system design cycle. This research forms part of a larger research programme which is concerned with the development of real-time process-control systems in which software is used to control concurrent physical processes. The general objective of the research in this thesis is to investigate the use of formal techniques in the analysis of such systems at their early stages of development, with a particular bias towards an application to high speed machinery. Specifically, the research aims to generate a standardised software development formalism for real-time process-control systems, particularly for software controller synthesis. In this research, a graphical modelling formalism called Sequential Function Chart (SFC), a variant of Grafcet, is examined. SFC, which is defined in the international standard IEC1131 as a graphical description language, has been used widely in industry and has achieved an acceptable level of maturity and acceptance. A comparative study between SFC and Petri nets is presented in this thesis. To overcome identified inaccuracies in the SFC, a formal definition of the firing rules for SFC is given. To provide a framework in which SFC models can be analysed formally, an extended time-related Petri net model for SFC is proposed and the transformation method is defined. The SFC notation lacks a systematic way of synthesising system models from the real world systems. Thus a standardised approach to the development of real-time process control systems is required such that the system (software) functional requirements can be identified, captured, analysed. A rule-based approach and a method called system behaviour driven method (SBDM) are proposed as a development formalism for real-time process-control systems.

Logic Based Pattern Recognition - Ontology Content (1)

* The research is supported partly by INTAS: 04-77-7173 project, http://www.intas.be

Analogous Reasoning and Case-based Reasoning for Intelligent Decision Support Systems

Methods of analogous reasoning and case-based reasoning for intelligent decision support systems are considered. Special attention is drawn to methods based on a structural analogy that take the context into account. This work was supported by RFBR (projects 02-07-90042, 05-07-90232).

Семантическая Википедия как Источник Онтологий для Интеллектуальных Поисковых Систем

Определены подходы к интеллектуальному поиску информации при помощи современных Web-технологий. Проанализированы источники онтологических описаний предметных областей поиска, в частности, семантическая Википедия. Предложены методы использования онтологий для повышения пертинентности информационного поиска.

Модельное Описание Процессов Развития: Механизмы, Структура, Система Целей, Индикаторы

В постановочном плане рассмотрены вопросы введения понятия «пространство развития», виды возможных изменений системы, структура и механизмы развития. Рассмотрены типологии индикаторов развития, роль информационной компоненты и понятия качества.

A framework for specification and analysis of software architectures

Software architecture is the abstract design of a software system. It plays a key role as a bridge between requirements and implementation, and is a blueprint for development. The architecture represents a set of early design decisions that are crucial to a system. Mistakes in those decisions are very costly if they remain undetected until the system is implemented and deployed. This is where formal specification and analysis fits in. Formal specification makes sure that an architecture design is represented in a rigorous and unambiguous way. Furthermore, a formally specified model allows the use of different analysis techniques for verifying the correctness of those crucial design decisions. ^ This dissertation presented a framework, called SAM, for formal specification and analysis of software architectures. In terms of specification, formalisms and mechanisms were identified and chosen to specify software architecture based on different analysis needs. Formalisms for specifying properties were also explored, especially in the case of non-functional properties. In terms of analysis, the dissertation explored both the verification of functional properties and the evaluation of non-functional properties of software architecture. For the verification of functional property, methodologies were presented on how to apply existing model checking techniques on a SAM model. For the evaluation of non-functional properties, the dissertation first showed how to incorporate stochastic information into a SAM model, and then explained how to translate the model to existing tools and conducts the analysis using those tools. ^ To alleviate the analysis work, we also provided a tool to automatically translate a SAM model for model checking. All the techniques and methods described in the dissertation were illustrated by examples or case studies, which also served a purpose of advocating the use of formal methods in practice. ^

Imunidade recíproca e livre concorrência: considerações acerca de sua fruição por empresas estatais

This study begins with a brief overview of tax immu nities in general, dealing with the concept, legal, doctrinal ratings and limits. Then enters into the reciprocal immunity, since its birth in the United States, its justifica tions, until her current developments in the Brazilian Supreme Court, which has expanded it quite considerably. That Court has extended to state owned enterprises, even if pa id by public prices or rates, or if acts somewhat away from its essential functions, es pecially if they are public services provider. Given this linkage, these are also treate d in own topic, grounded in newer doctrinal proposals and less attached to historical formalisms (see such Supremacy of Public Interest over Private one). Public services are approached in its diversity, oblivious to traditional monolithic nature and accu stomed to the modern doctrine of fundamental human rights. It deals also the princip les of free enterprise and free competition, given that the public service provider s have lived intensely in this environment, be they public or private agents. In d ialectical topic, these institutes are placed in joint discussion, all in an attempt to in vestigate their interactions and propose criteria less generic and removed from real ity, to assess the legitimacy of the mutual enjoyment of immunity by certain agents. Sev eral cases of the Court are analyzed individually, checking in each one the app lication of the proposed criteria, such logical-deductive activity and theory of pract ice approach. At the end, the conclusions refer to a reciprocal immunity less rhe torical and ideological and more pragmatic and consequentialist. It is proposed the end to the general rules or abstract formulas of subsumption, with concerns on the one h and the actual maintenance of the federal pact, and on the other by a solid econo mic order without inapt advantages to certain players, which flatly contradicts the co nstitutional premises.

Reasoning about change over time: Actions, events and their effects

This paper presents a new formalism for reasoning about change over time. The formalism derives a clean separation between the notion of states and situations. It allows more flexible temporal causal relationships than do other formalisms for reasoning about causal change, such as the situation calculus and the event calculus. It includes effects that start during, immediately after, or some time after their causes, and which end before, simultaneously with, or after their causes. A formal distinction between actions, action-types and events is proposed, which allows the expression of common-sense causal laws at high level. It is shown how these laws can be used to deduce state change over time at low level, when events occur under certain preconditions hold. Two problems that beset most interval-based temporal systems, i.e., the so-called dividing instant problem and intermingling problem, are absent from the formalism.

Zbadanie prądu tunelowego w złączach typu metal-nadprzewodnik trypletowy dla wybranych symetrii parametru porządku

Wydział Fizyki: Zakład Teorii Ciała Stałego

A Mapping-Scheduling Algorithm for Hardware Acceleration on Reconfigurable Platforms

Reconfigurable platforms are a promising technology that offers an interesting trade-off between flexibility and performance, which many recent embedded system applications demand, especially in fields such as multimedia processing. These applications typically involve multiple ad-hoc tasks for hardware acceleration, which are usually represented using formalisms such as Data Flow Diagrams (DFDs), Data Flow Graphs (DFGs), Control and Data Flow Graphs (CDFGs) or Petri Nets. However, none of these models is able to capture at the same time the pipeline behavior between tasks (that therefore can coexist in order to minimize the application execution time), their communication patterns, and their data dependencies. This paper proves that the knowledge of all this information can be effectively exploited to reduce the resource requirements and the timing performance of modern reconfigurable systems, where a set of hardware accelerators is used to support the computation. For this purpose, this paper proposes a novel task representation model, named Temporal Constrained Data Flow Diagram (TCDFD), which includes all this information. This paper also presents a mapping-scheduling algorithm that is able to take advantage of the new TCDFD model. It aims at minimizing the dynamic reconfiguration overhead while meeting the communication requirements among the tasks. Experimental results show that the presented approach achieves up to 75% of resources saving and up to 89% of reconfiguration overhead reduction with respect to other state-of-the-art techniques for reconfigurable platforms.

Methodology for Conceptualization of Customizable Virtual Workspaces

Part 12: Collaboration Platforms

Development and Implementation of the Plasma Focus Technology for Radiation Therapy Applications

A Plasma Focus device can confine in a small region a plasma generated during the pinch phase. When the plasma is in the pinch condition it creates an environment that produces several kinds of radiations. When the filling gas is nitrogen, a self-collimated backwardly emitted electron beam, slightly spread by the coulomb repulsion, can be considered one of the most interesting outputs. That beam can be converted into X-ray pulses able to transfer energy at an Ultra-High Dose-Rate (UH-DR), up to 1 Gy pulse-1, for clinical applications, research, or industrial purposes. The radiation fields have been studied with the PFMA-3 hosted at the University of Bologna, finding the radiation behavior at different operating conditions and working parameters for a proper tuning of this class of devices in clinical applications. The experimental outcomes have been compared with available analytical formalisms as benchmark and the scaling laws have been proposed. A set of Monte Carlo models have been built with direct and adjoint techniques for an accurate X-ray source characterization and for setting fast and reliable irradiation planning for patients. By coupling deterministic and Monte Carlo codes, a focusing lens for the charged particles has been designed for obtaining a beam suitable for applications as external radiotherapy or intra-operative radiation therapy. The radiobiological effectiveness of the UH PF DR, a FLASH source, has been evaluated by coupling different Monte Carlo codes estimating the overall level of DNA damage at the multi-cellular and tissue levels by considering the spatial variation effects as well as the radiation field characteristics. The numerical results have been correlated to the experimental outcomes. Finally, ambient dose measurements have been performed for tuning the numerical models and obtaining doses for radiation protection purposes. The PFMA-3 technology has been fully characterized toward clinical implementation and installation in a medical facility.