As technology evolves, the need to use software for critical applications increases. It is then required that this software will always behave correctly. Verification is the process of formally proving that a program is correct. Model checking is a technique used to perform verification, which has been successful with finite state concurrent programs. In the recent years, there has been progress in the area of the verification of infinite state concurrent programs. There can be several sources of infiniteness. Relevant to this thesis are recent model checking techniques developed at LiU, that can automatically establish correctness for programs manipulating variables that range over infinite domains, and spawning arbitrary many threads, which can synchronize using shared variables, barriers, semaphores etc. These techniques resulted in the tool PACMAN for the verification of multi-threaded programs. The aim of this thesis is to extract analyzable models from multi-threaded C programs, in order to use them for verifying the program that they describe, by using PACMAN. In addition, we augment the C programming language to allow the possibility of expressing some important concepts of multi-threaded programs, such as non-determinism, atomicity etc, with the use of the traditional C syntax. In a following step, we target PACMAN's input format, in order to verify our extracted models. Such verification engines usually accept as input the description of a multi-threaded program expressed in some modeling language. We, therefore, translate a minimum subset of the C programming language, which has been augmented, to effectively describe a multithreaded program, to PACMAN's input format and then pass the description to the engine. In the context of this thesis, we have successfully defined a set of annotation for the C programming language, in order to assist the description of multi-threaded programs. We have implemented a tool that effectively translates annotated C code into the modeling language of PACMAN. The output of the tool is later passed to the verification engine. As a result, we have contributed to the automation of verifying multi-threaded C programs.

The purpose of this project is to investigate RESS, Responive + Server Side, a startegy for serving optimized web content to different types of end user devices. RESS is also compared to other mutli-device targeting solutions, Responisve Web Design and Server Side Adaptation, from different points of view, such as performance and workload.

Är ett byte mellan språken R och PHP genomförbart, är det en bra idé att lägga kraft och tid på vid generering av diagram på en hemsida? När det kommer till att skapa en hemsida hjälper CodeIgniter till med strukturen, men det hjälper enbart om koden i sig sedan är väl strukturerad och välskriven. Att byta från ett litet språk som R till ett stort som PHP har sina fördelar, speciellt med att det är fler som kan PHP och kan gå in och hjälpa till om förändringar behövs. För att detta ska gå att genomföras på ett enkelt sätt krävs dock att den ursprungliga koden är välskriven.

No description available.

Konstruktion utav stora stadsmiljöer i 3D består, från idé till färdig scen, utav många olika processer och tekniker. Från koncept genom planering, modellering, texturering och rendering till slutresultatet. Det är därför önskvärt att minimera mängden onödigt arbete och effektivisera dessa processer där det är möjligt. Den här studien undersöker hur modularitet kan användas och implementeras i semi-automatiserade konstruktionslösningar i syftet för att användas i filmsammanhang. Kärnan utav studien utgår ifrån att en grafiker skapar diverse byggstenar för olika stadsmiljöer. För att sedan konstruera en miljö utifrån dessa byggstenar kan programvaror automatisera processen med hjälp av olika variabler som kontrolleras utav grafikern. Detta sparar grafikern enorma mängder repetitivt arbete som istället kan fokusera på detaljarbete och slutresultatet. Genom en mer automatiserad process skapas en bättre balans i arbetet mellan detaljrikedom och den spenderade arbetstiden, vilket ger ett mer effektiviserat arbetsflöde.

Abstract In most of the animation pipelines today, motion capture and different simulations e.g. Autodesk Maya Muscle is used to get a more realistic feel of an animation. The main goal of this Thesis is to make a character appear and move in as natural a way as possible and exploring different methods on receiving a good result. It will answer different question on how to record movement and using that data together with a system that simulates muscles. To complete this process we will record using a Microsoft Kinect Camera, which is originally hardware for Xbox movement software. For our muscle simulation we used Autodesk Maya Muscle, where we built a muscle system. This will be research through finding information on each subject separately and trough experiments combing the two together

Software is continually and rapidly evolving with constant risk of introducing faults. Software testing has long been used to aid in the detection of faults, and agile development strategies have been driving the use of automated tests and regression testing specifically. As development continues, test suites eventually grow in the number of test cases to the extent that the execution time is extensive. When it has increased to the point that it prevents efficient software engineering, a regression testing technique is required to reduce the feedback cycle times - the times for receiving feedback from tests on changes. This thesis has investigated regression testing techniques presented in previous research. The focus has been on test case selection techniques - for selecting a subset of all test cases for execution - and test case prioritization techniques - for determining the execution order of test cases. With some evaluation criteria in mind, a safe modification-based selection and prioritization technique was chosen and a proof-of-concept implementation was developed. First, the implemented technique was evaluated for robustness using an example application. Following, a case study was conducted on an existing software development project, where the perceived problems with regression testing were documented by interviewing a software developer. The technique was then integrated with the project's existing regression testing and its efficiency was evaluated. It was concluded that a regression testing technique is, to some extent, practical to implement, although difficult to verify for complete correctness. Empirical evaluations in the case study showcased reduced feedback cycle times of 60% or more compared to when not using the technique - assuming a uniform distribution of failing test cases. However, it was stated as important to evaluate the efficiency of the technique on a per-project basis.

Context Inference and Planning are becoming more and more valuable in robot oriented technology and several artificial intelligence techniques exist for solving both context inference and planning problems. However, not many combinations of context inference and planning solving have been tried and evaluated as well as comparison between these combinations. This thesis aims to compare two different algorithms, using two different approaches to the problems of context inference and planning. The algorithms studied are Graphplan, which is a classical planning approach to context inference and planning, and SAM, a framework created by the Örebro University, that uses a temporal constraint-based approach. It will also evaluate the expressiveness of these two algorithms applied to the system. To do so an implementation and test of the two approaches is evaluated on a real robot system. This evaluation will show that SAM is much more expressive in terms of domain definition than Graphplan and that reasoning about temporal constraints could become crucial for achieving a system that can succesfully recognize context inference and plan accordingly. The decision on whether to apply one or another is just depending on the kind of system the user needs. If temporal constraints are mandatory, then SAM is the choice to make; in case the only thing the system needs is a fast algorithm able to always find a plan, if it exists, then Graphplan is a better choice.

Detta arbete har genomförts i samarbete med Försvarsmakten och behandlar vilka möjligheter som finns för forensiska undersökningar av e-boksläsaren Amazon Kindle. I arbetets litteraturstudie beskrivs hur tidigare forskning inom ämnet är kraftigt begränsad. Arbetet syftar därför till att besvara hur data kan extraheras från en Kindle, vilka data av forensiskt intresse en Kindle kan innehålla, var denna information lagras och om detta skiljer sig åt mellan olika modeller och firmware-versioner samt om det är nog att undersöka endast den del av minnet som är tillgänglig för användaren eller om ytterligare privilegier för att komma åt hela minnesarean bör införskaffas. För att göra detta fylls tre olika modeller av Kindles med information. Därefter tas avbilder på dem, dels på endast användarpartitionen och dels på dess fullständiga minnesarea efter att en privilegie-eskalering har utförts. Inhämtad data analyseras och resultatet presenteras. Resultatet visar att information av forensiskt intresse så som anteckningar, besökta webbsidor och dokument kan återfinnas, varför det finns ett värde i att utföra forensiska undersökningar på Amazon Kindles. Skillnader råder mellan vilken information som kan återfinnas och var den lagras på de olika enheterna. Enheterna har fyra partitioner varav endast en kan kommas åt utan privilegie-eskalering, varför det finns en fördel med att inhämta avbilder av hela minnesarean. Utöver ovanstående presenteras en metod för att förbipassera en enhets kodlås och därigenom få fullständig åtkomst till den även om den är låst. / This work have been done in cooperation with the Swedish Armed Forces (Försvarsmakten) and presents what possibilities there are for forensic investigations of the e-book reader Amazon Kindle. In its literature study it is described how previous research in the field is very limited. The work is therefore aiming to answer what data of forensic interest a Kindle can contain and how it can be extracted, where this information is stored and if this differs between different models and firmware versions, as well as if it's enough to investigate only the part of the memory that is available for the user or if further privileges to reach the whole memory area needs to be obtained. To do this, three different models of Kindles is filled with information. After that data images are taken off them, first on only the user partition and then on the whole memory area after a privilege escalation have been performed. Gathered data is analyzed and the result is presented. The result shows that information of forensic interest such as notes, visited web sites and documents can be found and there is therefore a value in performing forensic investigations on Amazon Kindles. There is a difference between what information that can be found and where it's stored on the different units. The units have four partitions of which only one is accessible without privilege escalation. Because of this there is an advantage of obtaining images of the whole memory area. In addition to the above a method for bypassing the device code of a unit and thereby getting complete access to it even though it is locked is presented.

Web applications an play increasingly central role in our every day life, as many of our computer based tasks are performed solely within the web browser. Desktop applications requiring installation is becoming part of the past and most applications gets a web alternative — turning the web into a target platform for application development. A complication with this is that the web lack the performance of native applications, motivating a need for something more powerful. This thesis investigates different technologies that aim to solve this problem by allowing developers to create native web applications, that allow web applications to use native capabilities. Two such technologies are Xax and Native Client (NaCl), which allow web applications to run compiled native code in the web browser, while still providing the portability across operating systems. In addition to the investigation a case study of how Portable Native Client (PNaCl) is to use for creating a native web application. A performance analysis is presented in order to determine how large the performance gains are with native web applications compared to traditional. The results show that NaCl performance is far superior to JavaScript, and very close to native speeds. Native Client is a great technology, both for migrating legacy C/C++ applications to the web and for creating high performance native web applications. The biggest challenge for Native Client is to get accepted by other browser manufacturers