Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine-checked proofs of standard algebraic and congruence properties of bisimilarity apply to every instance of the framework. The contribution of this licentiate thesis is to significantly extend the applicability and expressiveness of psi-calculi by incorporating several advanced language features into the framework: broadcasts, higher-order communication, generalised pattern matching, sorts and priorities. The extensions present several interesting technical challenges, such as negative premises. The machine-checked proofs for standard results about bisimilarity are generalised to each of these new settings, and the proof scripts are freely available online. / UPMARC

Transparency is a key principle in democratic societies. For example, the public sector is in part kept honest and fair with the help of transparency through different freedom of information (FOI) legislations. In the last decades, while FOI legislations have been adopted by more and more countries worldwide, we have entered the information age enabled by the rapid development of information technology. This has led to the need for technological solutions that enhance transparency, for example to ensure that FOI legislation can be adhered to in the digital world. These solutions are called transparency-enhancing tools (TETs), and consist of both technological and legal tools. TETs, and transparency in general, can be in conflict with the privacy principle of data minimisation. The goal of transparency is to make information available, while the goal of data minimisation is to minimise the amount of available information. This thesis presents two privacy-preserving TETs: one cryptographic system forenabling transparency logging, and one cryptographic scheme for storing the data for the so called Data Track tool at a cloud provider. The goal of the transparency logging TET is to make data processing by data controllers transparent to the user whose data is being processed. Our work ensures that the process in which the data processing is logged does not leak sensitive information about the user, and thatthe user can anonymously read the information logged on their behalf. The goal of the Data Track is to make it transparent to users which data controllers they have disclosed data to under which conditions. Furthermore, the Data Track intends to empower users to exercise their rights, online and potentially anonymously, with regard to their disclosed data at the recipient data controllers. Our work ensures that the data kept by the Data Track can be stored at acloud storage provider, enabling easy synchronisation across multiple devices, while preserving the privacy of users by making their storage anonymous toward the provider and by enabling users to hold the provider accountable for the data it stores.

Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. This thesis presents broadcast psi-calculi and higher-order psi-calculi, two extensions of the psi-calculi framework, allowing respectively one-to-many communications and the use of higher-order process descriptions through conditions in the parameterised logic. Both extensions preserve the purity of the psi-calculi semantics; the standard congruence and structural properties of bisimilarity are proved formally in Isabelle. The work going into the extensions show that depending on the specific extension, working out the formal proofs can be a work-intensive process. We find that some of this work could be automated, and implementing such automation may facilitate the development of future extensions to the psi-calculi framework. / UPMARC

I det här arbetet utvecklades en androidapplikation åt ett företag. Målet med applikationen var att den skulle vara en kopia av en befintlig iOS-applikation. Parallellt med applikationsutvecklingen utfördes också en analys av informationssäkerheten i systemet kring applikationen. Målet för analysen var att undersöka vilka risker som fanns och ge förslag på hur de kunde åtgärdas. Analysen utfördes med hjälp av en metod framtagen för just detta arbete vilken kom att kallas Säkerhetsanalys. Metoden baserades på Facilitated Risk Analysis and Assessment Process. Med hjälp av Säkerhetsanalysen kunde två typer av information identifieras, användar-information och applikationsinformation samt tre situationer då informationen var utsatt för hot. Situationerna var vid lagring i telefonen, vid lagring på servern och under överföring mellan dessa enheter. Det största hotet var avlyssning vid överföring och att då byta från HTTP till HTTPS skulle näst intill helt eliminera det hotet. Slutsatsen författarna drog var att med relativt enkla medel kunde informationssäkerheten ökas markant. I utvecklingsarbetet användes den agila metoden scrum. Resultatet av applikationsutvecklingen var en applikation som implementerade de grundfunktioner som nämns i kravspecifikationen.

Det finns idag många verktyg och ramverk för att utveckla spelapplikationer. I den här rapporten kommer jag utvärdera Phaser.io som är ett öppen källkodsramverk för att utveckla webspelsapplikationer. Resultatet av det här examensarbetet är en prototyp av spelet Equamem som jag har utvecklat utifrån min handledare Erik Berglunds spelkoncept och design. Equamem är en HTML5 webspelsprototyp utvecklat med ramverket Phaser.io med HTML5 och JavaScript. I rapporten kommer jag gå igenom olika designval som gjorts och itererats under spelprototypens versioner av utveckling. Jag kommer även utforska hur man utvecklar ett intressant och lättlärt matematikpusselspel. Rapporten kommer innehålla information om Phaser.io, vad det är och vad det erbjuder för funktionalitet och hur jag har använt det i utvecklingen av Equamem. Jag kommer gå igenom fördelar och nackdelar med att använda ramverkets funktioner och utvärdera hur väl lämpat det har för att utveckla spel som Equamem.

There are several applications which make it possible for users to search and find their favorite channels; these channels could be anything such as TV channels, radio channels, blogs, websites, etc. Is a graph-based interface more efficient than a traditional one for channel discovery? The aim of this thesis is to answer the question by developing a new browsing method in a graphical user-friendly interface and compare it with a traditional hierarchical method. A graphical application is a graph-based application, in which the nodes (or vertices) represent channels and the edges represent the links among channels. The graphical application is built with the newest Hypertext Markup Language Standard (HTML5) and Cascading Style Sheets (CSS3). A large part of the graphical application is built using the JavaScript library Sigma.js. The resulting graphical application is tested with users and compared with the traditional hierarchical user interface. A questionnaire is provided for end-users to gather feedback. After analyzing the participant‟s feedback, the results were surprising and interesting. A majority of participants enjoyed interacting with graphical application, and they were interested to use it in the future. The final result is merged into the thesis report. This thesis includes all the work of creating graphical and hierarchical user interfaces, testing the hierarchical and graphical user interfaces, and analyzing the user‟s feedback.

No description available.

Den här rapporten beskriver ett examensarbete som genomfördes åt Flex Datasystem med syfte att vidareutveckla Flex HRM mobile. Vår uppgift var att implementera projektrapportering som ingår i modulen Flex Tid, vilket innebär att användaren kan registrera eller redigera diverse projekt via mobila enheter. Vi använde oss av JavaScript, HTML5, CSS3 och även diverse ramverk för att fullfölja vårt arbete. / This report describes a thesis conducted at Flex Datasystem with a view to further developing Flex HRM mobile. Our task was to implement the project reporting in the module Flex Tid, which means that users can register or edit various projects via mobile devices. We used JavaScript, HTML5, CSS3 and also various frameworks to pursue our work.

No description available.

Fire fighting operations, sometimes, can put the life of fire fighters in threat. For example an environment with potential fire risk and with the presence of gas bottles can cause an explosion, besides other dangers, and certainly put the life of both the victims and fire fighters at risk. Recent advancements in the field of robotics enabled to develop a robotic system which can assist the fire fighters to avoid any human injury and property damage. The live update of the map displayed on the operator’s screen, while teleoperating the robot for search process, can help to properly plan the rescue operation. This thesis details the implementation of a rich 2D mapping system for FUMO2 a fire fighting assistant robot developed by AB Realisator. Rich 2D mapping system produces an occupancy grid map, having the geometry and temperature of the environment with position of fire extinguishers, by fusing different sensor modalities. By rich we mean any type of additional information on top of the standard, geometric only, 2D maps. A sensor fusion method is proposed to integrate the distance measurements reported by a laser range finder, temperature readings acquired by a thermal IR camera and the position of fire extinguishers delivered by visible spectrum camera based object detector. The object detector detects the object in real time and is developed utilizing the technique of cascade of boosted classifiers using MB-LBP features. The proposed system is implemented on both FUMO2 a fire fighting assistant robot and in Gazebo simulator for testing and evaluation.