| 1. |
- Carlson, Jan, 1976-
(författare)
-
Event Pattern Detection for Embedded Systems
- 2007
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Events play an important role in many computer systems, from small reactive embedded applications to large distributed systems. Many applications react to events generated by a graphical user interface or by external sensors that monitor the system environment, and other systems use events for communication and synchronisation between independent subsystems. In some applications, however, individual event occurrences are not the main point of concern. Instead, the system should respond to certain event patterns, such as "the start button being pushed, followed by a temperature alarm within two seconds". One way to specify such event patterns is by means of an event algebra with operators for combining the simple events of a system into specifications of complex patterns.This thesis presents an event algebra with two important characteristics. First, it complies with a number of algebraic laws, which shows that the algebra operators behave as expected. Second, any pattern represented by an expression in this algebra can be efficiently detected with bounded resources in terms of memory and time, which is particularly important when event pattern detection is used in embedded systems, where resource efficiency and predictability are crucial.In addition to the formal algebra semantics and an efficient detection algorithm, the thesis describes how event pattern detection can be used in real-time systems without support from the underlying operating system, and presents schedulability theory for such systems. It also describes how the event algebra can be combined with a component model for embedded system, to support high level design of systems that react to event patterns.
|
|
| 2. |
- Gu, Rong, 1987-
(författare)
-
Automatic Model Generation and Scalable Verification for Autonomous Vehicles : Mission Planning and Collision Avoidance
- 2020
-
Licentiatavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Autonomous vehicles such as mobile driver-less construction equipment bear the promise of increased safety and industrial productivity by automating repetitive tasks and reducing manual labor costs. These systems are usually involved in safety- or mission-critical scenarios, therefore they require thorough analysis and verification. Traditional approaches such as simulation and prototype testing are limited in their scope of verifying a system that interacts autonomously with an unpredictable environment that assumes the presence of humans and varying site conditions. Methods for formal verification could be more suitable in providing guarantees of safe operation of autonomous vehicles within specified unpredictable environments. However, employing them entails addressing two main challenges: (i) constructing the models of the systems and their environment, and (ii) scaling the verification to the incurred model complexity. We address these two challenges for two essential aspects of autonomous vehicle design: mission planning and collision avoidance. Though inherently different, communication between these two aspects is necessary, as the information obtained from verifying collision avoidance can help to improve the mission planning and vice versa. Finding a solution that addresses both mission planning and collision avoidance modeling and verification, while decoupling them for solution maintainability is one crux of this study. Another one deals with demonstrating the applicability and scalability of the proposed approach on complex and industrial-level systems.In this thesis, we propose a two-layer framework for mission planning and verification of autonomous vehicles. The framework separates the modeling and computing mission plans in a discrete environment, from the vehicle movement within a continuous environment, in which collision avoidance algorithms based on dipole fields are proven to ensure safe behavior. We call the layer for mission planning, the "static layer", and the other one the "dynamic layer". Due to the inherent difference between the layers, we use different modeling and verification approaches, namely: (i) the timed automata formalism and the UPPAAL model checker to compute mission plans for the autonomous vehicles, and (ii) hybrid automata and statistical model checking using UPPAAL Statistical Model Checker to verify collision avoidance and safe operation. We create model-generation algorithms, based on which we develop tool support for the static layer, called TAMAA (Timed-Automata-Based Planner for Autonomous Agents). The tool enables the designers to configure their systems and environments in a graphical user interface, and utilize formal methods and advanced path-planning algorithms to generate mission plans automatically. TAMAA also integrates reinforcement learning with model checking to alleviate the state-space explosion problem when the number of vehicles increases. We create a hybrid model for the dynamic layer of the framework and propose a pattern-based modeling method for the embedded control systems of the autonomous vehicles to ease the design and facilitate reuse. We validate the proposed framework and design method on an industrial use case involving autonomous wheel loaders, for which we verify invariance, reachability, and liveness properties.
|
|
| 3. |
- Gilenstam, Kajsa, 1974-
(författare)
-
Gender and physiology in ice hockey : a multidimensional study
- 2009
-
Doktorsavhandling (övrigt vetenskapligt/konstnärligt)abstract
- Background That men are prioritised over women has been called the “gender regime in sport”, and has in part been explained by the gender difference in performance. However, gender differences in physical performance between women and men can be debated to depend on how comparisons are made and on the fact that there are many different confounders that may influence the results. Even if attempts are made to overcome this and the groups of women and men are stated to be matched, there are still often differences in training experience in years, or differences in training load. Women tend to have less experience in ice hockey in relation to age and differences in training conditions have also been reported. The aim of this thesis was to investigate how female and male ice hockey players position themselves in their sport and to visualise the interactions between society and biology that may affect performance. Theoretical approach and methods Harding’s three perspectives (Symbolic, Structural and Individual) were applied on information from team administration as well as on results from questionnaires, semi-structured interviews, and tests of puck velocity, anthropometrics, body composition, isokinetic muscle strength, ergospirometry and on-ice tests from female and male ice hockey players. Results Vast differences in structural conditions were found, for example in hockey history and in the financial situation within the teams and both women and men were aware of the gender differences in structural conditions. However these differences were not even considered when comparisons of the ice hockey performance of women and men were made. Nine out of ten female players increased puck velocity when a more flexible stick and a lighter puck were used thus indicating that poorly adjusted equipment may affect performance. Male ice hockey players were taller, heavier and stronger, had more lean body mass and a higher aerobic capacity compared to the women in absolute values as well as in relation to body weight. However, the differences diminished or disappeared when the values were expressed in relation to lean body mass. Men had higher expectations on their situation as athletes and the interviewed women described men’s ice hockey as superior to theirs and consequently male ice hockey players deserved better conditions. Conclusions The views of women and men may affect structural conditions in sport which in turn may affect possibilities in sport for the individual. Gender differences in conditions thus risk confirming the traditional views of femininity and masculinity. However, by moving outside the normal gender boundaries individuals may change the traditional views of femininity and masculinity.
|
|
