Modeling and Assessment of Systems Security (2009)
Jonas Hallberg, Johan Bengtsson, Niklas Hallberg
Information technology (IT) is a crucial resource and enabler in almost every part of our society. However, there are severe risks associated with IT that may substantially decrease the potential...
Mare Nostrum - A study of the oil priceâs effect on Danish shipping companies (2009)
Large shipping vessels currently got no other valid source of fuel than the ones that are oil based. Crude oil hence becomes an essential necessity for the shipping industry. This thesis examines the...
Skivförpackningar–en studie om konsumentval (2009)
Denna rapport är en konsumentundersökning rörande skivförpackningar. Syftet med undersökning är att ta reda på vad konsumenter har för attityd, tankar och känslor kring olika slags...
Vilken betydelse har Celebrity Endorsement för företagens marknadsföringsstrategi? (2009)
Andersson, Carl-Henrik, Bengtsson, Johan, Jonsson, Robin
Vilken betydelse har Celebrity Endorsement för företagens marknadsföringsstrategi?Problemformuleringen leder fram till syftet med uppsatsen. Vi kommer nedan att dela upp syftet i tre punkter och...
Bengtsson, Johan, Bixberg, Tobias
Den svenska arbetsmarknaden är under förändring och blir mer individualiserad och flexibel. Lagen om anställningsskydd blir mer ifrågasatt och det finns diskussioner om att förändra denna lag....
Protecting Mac OS X Restricting use on the x86 platform (2008)
Johan Bengtsson, Supervisor Viiveke Fåk, Love Thyresson, Johan Bengtsson, Love Thyresson
In late autumn 2005 Apple Computers announced that they would switch their entire computer product line to Intel processors. Along with the decision came an announcement that the Mac OS X operating...
Marco Tirado, Daniel Friman, Linda Klevard, Johan Bengtsson, Lin Ji
We want thank our project assistant Sha Jao and also Per Zetterberg.
Utveckling av Prisjakts butiksomdömessystem (2008)
This thesis work is the result of the company Prisjaktâs wish to develop and improve its current system of opinions for online stores. The challenge was to develop a similar system that...
Bengtsson, Johan, Brinck, Peter
There is no debate over the importance of IT security. Equally important is the research on security assessment; methods for evaluating the security of IT systems. The Swedish Defense Research Agency...
Bengtsson, Johan, Brinck, Peter
There is no debate over the importance of IT security. Equally important is the research on security assessment; methods for evaluating the security of IT systems. The Swedish Defense Research Agency...
UPPAAL: Model checking Timed Automata (2008)
Gerd Behrmann, Re David, Kim G. Larsen, M. Oliver Möller, Paul Pettersson, Wang Yi, ...
x ≤ 5 x = = 5 count: = count+1 clock x; int count network of timed automata discrete data types arrays hand-shake synchronization urgency C count = = 3 D template mechanism committed locations...
UPPAAL: Model checking Timed Automata (2008)
Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D’argenio, Re David, Ansgar Fehnker, ...
count: = count +1 x: = 0 A B x = = 5 clock x; int count x < = 5 Only subset of TCTL supported: E<> ϕ reachability A[] ϕ safety (invariantly ϕ) E[] ϕ possibly always ϕ A<> ϕ...
Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi
Uppaal 1 is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata [12, 9, 4], developed during the past two...
Automatic Verification of Real--Time Systems (2007)
Kim G. Larsen, Paul Pettersson, Wang Yi, Johan Bengtsson, Johan Bengtsson, Kim Larsen, ...
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...
Measures under Pressure- Applicable Types of Performance Measurements for (2007)
School Of Economics, Commercial Law, Johan Bengtsson, Jörg Jung
Measures under Pressure In today’s business environment concepts such as stakeholder value and service management have become extremely important to satisfy employees, customers and shareholders....
Bengtsson, Johan, Edebol, Johannes
Context. This thesis takes an opportunity perspective. Radio Frequency Identification technology (RFID) has showed potential in enhancing and optimizing supply chains. For Pan Nordic Logistics (PNL),...
Bengtsson, Johan, Edebol, Johannes
Context. This thesis takes an opportunity perspective. Radio Frequency Identification technology (RFID) has showed potential in enhancing and optimizing supply chains. For Pan Nordic Logistics (PNL),...
Chief Information Officer : A business strategy resource? (2007)
Forsberg, Niclas, Wahlberg, Lars-Åke, Bengtsson, Johan
This thesis aims at describing the CIO role from the perspective of two interviews and the literature on the subject. Our research questions mainly focus on the actual work of a CIO and are answered...
Chief Information Officer : A business strategy resource? (2007)
Forsberg, Niclas, Wahlberg, Lars-Åke, Bengtsson, Johan
This thesis aims at describing the CIO role from the perspective of two interviews and the literature on the subject. Our research questions mainly focus on the actual work of a CIO and are answered...
The study investigates David Livingstone's views regarding the native population while traveling Africa. By using an inductive method generated from the material at hand, passages from his journal is...
Vad innebär kundlojalitet mer än att kunden gör återköp? (2007)
Begreppet kundlojalitet förknippas oftast med att ett företag har skaffat sig återköpare. En återköpare kan fås på många olika sätt. I uppsatsen behandlas fem kategorier som alla har...
Microwave Wireless Communication System (2006)
Dagne, Carl, Bengtsson, Johan, Lindgren, Ingemar
The purpose of the project was to develop the hardware to a microwave wireless system working at the frequency 2.45 GHz. The functionality of the system should also be easy to understand since the...
Strandh, Petter, Bengtsson, Johan, Johansson, Rolf, Tunestål, Per, Johansson, Bengt
Autoignition of a homogeneous mixture is very sensitiveto operating conditions. Therefore fast combustion phasingcontrol is necessary for reliable operation. There areseveral means to control the...
Strandh, Petter, Bengtsson, Johan, Johansson, Rolf, Tunestål, Per, Johansson, Bengt
Autoignition of a homogeneous mixture is very sensitiveto operating conditions. Therefore fast combustion phasingcontrol is necessary for reliable operation. There areseveral means to control the...
Closed-Loop Control of HCCI Engine Dynamics (2004)
The topic of the thesis is control of Homogeneous Charge Compression Ignition (HCCI) engine dynamics. HCCI offers a potential to combine high efficiency with very low emissions. In order to fulfill...
Cycle-to-cycle Control of a Dual-Fuel HCCI Engine (2004)
Strandh, Petter, Bengtsson, Johan, Johansson, Rolf, Tunestål, Per, Johansson, Bengt
A known problem of the HCCI engine is its lack of direct control andits requirements of feedback control. Today there exists severaldifferent means to control an HCCI engine, such as dual...
Bengtsson, Johan, Strandh, Petter, Johansson, Rolf, Tunestål, Per, Johansson, Bengt
Homogeneous charge compression ignition (HCCI) is a hybrid of the sparkignition and compression ignition engine concepts. As in a sparkignition engine, a homogeneous fuel-air mixture is created in...
System Identification of Homogenous Charge Compression Ignition (HCCI) Engine Dynamics (2004)
Bengtsson, Johan, Strandh, Petter, Johansson, Rolf, Tunestål, Per, Johansson, Bengt
Homogeneous Charge Compression Ignition (HCCI) combustion lacksdirect ignition timing control, instead the auto ignition depends on the operatingcondition. Since auto ignition of a homogeneous...
Modeling of HCCI Engine Combustion for Control Analysis (2004)
Bengtsson, Johan, Gäfvert, Magnus, Strandh, Petter
Operation of homogeneous charge compression ignition (HCCI) enginesare very sensitive to timing variations in the combustion of theair-fuel charge mixture and require precise control of the...
Control of Homogeneous Charge Compression Ignition (HCCI) Engine Dynamics (2004)
Bengtsson, Johan, Strandh, Petter, Johansson, Rolf, Tunestål, Per, Johansson, Bengt
The Homogeneous Charge Compression Ignition (HCCI) combustionconcept lacks direct ignition timing control, instead the autoignition depends on the operating condition. Since auto ignition of...
Software Technology Timed Automata: Semantics, Algorithms and Tools (2004)
in July 1992. UNU-IIST is jointly funded by the Governor of Macau and the governments of the People’s Republic of China and Portugal through a contribution to the UNU Endownment Fund. As well as...
Timed Automata: Semantics, Algorithms and Tools (2004)
Abstract. This chapter is to provide a tutorial and pointers to results and related work on timed automata with a focus on semantical and algorithmic aspects of verification tools. We present the...
Ion Current Sensing for HCCI Combustion Feedback (2003)
Strandh, Petter, Christensen, Magnus, Bengtsson, Johan, Johansson, Rolf, Vressner, Andreas, Tunestål, Per, ...
Measurement of ion current signal from HCCI combustionwas performed. The aim of the work was to investigateif a measurable ion current signal exists and if it is possible to obtain useful information...
Visual Position Tracking using Dual Quaternions with Hand-Eye Motion Constraints (2003)
Olsson, Tomas, Bengtsson, Johan, Robertsson, Anders, Johansson, Rolf
In this paper a method for contour-based rigid body tracking with simultaneouscamera calibration is developed. The method works for a singleeye-in-hand camera with unknown hand-eye...
Wp Modelling, P. Bouyer, P. Madhusudan, P. R. D’argenio, B. Jeannet, H. E. Jensen, ...
P. Bouyer. Untameable timed automata!. In Proc. 20th Ann. Symp.
Force Control and Visual Servoing Using Planar Surface Identification (2002)
Olsson, Tomas, Bengtsson, Johan, Johansson, Rolf, Malm, Henrik
When designing flexible multi-sensor based robot systems, one important problem is how to combine the measurements fromdisparate sensors such as cameras and force sensors. In this paper,we present a...
Variable Time Delays in Visual Servoing and Task Execution Control (2002)
Bengtsson, Johan, Haage, Mathias, Johansson, Rolf
We study an image-based visual servoing system implemented on a non-dedicatednetwork with non-deterministic computationalnodes. A problem is thattime delays aretypically non-deterministic and...
Modeling of Driver's Longitudinal Behavior (2002)
Bengtsson, Johan, Johansson, Rolf, Sjögren, Agneta
In the last years, many vehicle manufacturers have introduced advancedriver support in some of their automobiles. One of those new featuresis Adaptive Cruise Control (ACC), which extends the...
Clocks, DBMs and states in timed systems / (2002)
Thesis (doctorate)--Uppsala University, 2002.
Automated Analysis of an Audio Control Protocol Using (2002)
Uppaal Johan Bengtsson, Johan Bengtsson, K Are, J. Kristoffersen, ...
this paper we present a case-study where the tool Uppaal is extended and applied to verify an Audio-Control Protocol developed by Philips. The size of the protocol studied in this paper is...
Automated Verification of an Audio Control Protocol Using UPPAAL (2002)
Johan Bengtsson, Kåre J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, ...
In this paper we present a case-study in which the tool Uppaal is extended and applied to verify an Audio-Control Protocol developed by Philips. The size of the protocol studied in this paper is...
UPPAAL Implementation Secrets (2002)
Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim G. Larsen, Paul Pettersson, Wang Yi
In this paper we present the continuous and on-going development of datastructures and algorithms underlying the veri cation engine of the tool Uppaal. In particular, we review the datastructures of...
Modeling of Drivers Longitudinal Behavior (2001)
Bengtsson, Johan, Johansson, Rolf, Sjögren, Agneta
In the last years, many vehicle manufacturers have introduced advancedriver support in some of their automobiles. One of those new featuresis Adaptive Cruise Control (ACC), which extends the...
A Robot Playing Scrabble Using Visual Feedback (2001)
Bengtsson, Johan, Ahlstrand, Anders, Nilsson, Klas, Robertsson, Anders, Olsson, Magnus, Heyden, A., ...
Today most industrial robot systems use dedicated and rather limited sensors, and available control systems provide limited support for feedback control. Aiming towards more autonomous robot systems,...
Efficient Symbolic State Exploration of Timed Systems: (2001)
Johan Bengtsson, Johan Bengtsson, Johan Bengtsson
Timing aspects are important for the correctness of safety-critical systems. It is crucial that they are carefully analysed in designing such systems. UPPAAL is a tool designed to automate the...
Reducing memory usage in symbolic state-space exploration for timed systems (2001)
Johan Bengtsson, Johan Bengtsson
One of the major problems to scale up model checking techniques to the size of industrial systems is the large memory consumption. This report address the problem in the context of verifiers for...
Uppaal-now, next and future (2001)
Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R. D'argenio, Alexandre David, Ansgar Fehnker, ...
6 Wang Yi 1 1
In today's business environment concepts such as stakeholder value and service management have become extremely important to satisfy employees, customers and shareholders. This thesis focuses on how...
Partial Order Reductions for Timed Systems (1998)
Bengtsson, Johan, Jonsson, Bengt, Lilius, Johan, Yi, Wang
http://www.tucs.fi/Publications/proceedings/pBeJoLiYi98a.php
Partial order reductions for timed systems (1998)
Johan Bengtsson, Bengt Jonsson, Johan Lilius, Wang Yi
Abstract. In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit clock...
Partial Order Reductions for Timed Systems (1998)
Johan Bengtsson, Bengt Jonsson, Johan Lilius, Wang Yi
. In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit clock...
Partial Order Reductions for Timed Systems (1998)
Johan Bengtsson, Bengt Jonsson, Johan Lilius, Wang Yi
. In this paper, we present a partial-order reduction method for timed systems based on a local-time semantics for networks of timed automata. The main idea is to remove the implicit...
New Generation of UPPAAL (1998)
Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, Yi Wang, Carsten Weise
. Uppaal is a tool-set for the design and analysis of real-time systems. In [6] a relatively complete description of Uppaal before 1997 has been given. This paper is focused on the most recent...
Partial Order Reductions for Timed Systems (1998)
Johan Bengtsson, Bengt Jonsson, Johan Lilius, Wang Yi
Partial-order reduction has been successfully applied to state-space exploration for untimed systems, often yielding substantial reductions in the usage of time and memory. However, for timed systems...
Automata and Hybrid Systems (1998)
Professor Boris Trakhtenbrot, Lars Thalmann, Gustaf Naeser, Paul Pettersson, Johan Bengtsson, Edited Faron Moller, ...
this paper, Deterministic Latency Delay (Definition 3) is similar to our Filter; it is an operator.
Wang Yi, Johan Bengtsson, Johan Bengtsson, Kim G. Larsen, Kim G. Larsen, Fredrik Larsson, ...
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...
Verification of an Audio Protocol with Bus Collision Using UPPAAL (1996)
Johan Bengtsson, Kare J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, ...
. In this paper we apply the tool Uppaal 1 to an automatic analysis of a version of the Philips Audio Control Protocol with two senders and bus collision handling. This case study is significantly...
Uppaal: a Tool Suite for Validation and Verification of Real-Time Systems (1996)
Johan Bengtsson, Fredrik Larsson, Paul Pettersson, Wang Yi, Palle Christensen, Jesper Jensen, ...
The purpose of this document is to provide a complete description of Uppaal, including its theoretical basis and user guide. Uppaal is a tool suite for simulation and verification of real-time...
UPPAAL - a Tool Suite for Automatic Verification of Real-Time Systems (1996)
Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi
. Uppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a graphical interface that...
Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi
ABSTRACT Uppaal 1 is a tool suite for automatic veri cation of safety and bounded liveness properties of real-time systems modeled as networks of timed automata [12, 9, 4], developed during the past...
Verification of an audio protocol with bus collision using Uppaal (1996)
Johan Bengtsson, Kare J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, ...
In this paper we apply the tool Uppaal to an automatic analysis of a version of the Philips Audio Control Protocol with two senders and bus collision handling. This case study is significantly larger...
Johan Bengtsson, Johan Bengtsson, Kim G. Larsen, Kim G. Larsen, Fredrik Larsson, Fredrik Larsson, ...
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent...
UPPAAL - a Tool Suite for Symbolic and Compositional Verification of Real-Time Systems (1995)
Johan Bengtsson, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi
this document was written, we are in progress of modifying the description of the audio protocol presented in [6]. 4 Availability A full release should be available after summer 1995. A fi--release...
Uppaal: a tool-suite for automatic verification of real-time systems (1995)
Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, Wang Yi
Uppaal is a tool suite for automatic verification of safety and bounded liveness properties of real-time systems modeled as networks of timed automata. It includes: a graphical interface that...
[RS-96-60] Abstract, PostScript, PDF. (1995)
P. S. Thiagarajan, Igor Walukiewicz, An Expressively Complete, Johan Bengtsson, Kim G. Larsen, ...
in Margaria and Steffen, editors, Tools and Algorithms for The
Uppaal - a Tool Suite for Automatic Verification of Real-Time Systems (1995)
Kim G. Larsen, Johan Bengtsson, Johan Bengtsson, Kim Larsen, Fredrik Larsson, Fredrik Larsson, ...
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent...
Thesis (doctoral)--University of Lund, 1988.