A home automation system usually contains a set of tools that users use to control devices in their homes, often remotely. These devices often include but are not limited to light switches, thermostats, thermometers, window blinds, and climate controls. The potential for these kinds of systems is huge because of the sheer number of devices that could be controlled and managed with minimal and inexpensive extra hardware. Many of the appliances in a normal home could benefit from being connected to a system that allows the owner to manage and control the devices in their home. Thus the number of potential devices is orders of magnitude larger than the number of homes connected to the system. There are several systems on the market that provide systems to monitor and control a home environment, however these systems only support specific in system devices. This uncovers a problem where a homeowner only has the opportunity to use specific products that fit into these systems. By introducing an open platform for the public that are not bound to any system we can allow more devices to be integrated in the home and contribute to further development of smarter homes. The goal with this project was to provide a scalable open platform with the possibility of asynchronous updating. This has been done by implementing multiple logical parts to both provide a web interface for the user and to allow us to handle communication and storage of data. All these parts are linked together to form a system of servers that handles all background operations. This thesis discusses and presents implementations of all of these servers, how they are implemented, communicate with each other, provide secure connections and how they can scale with increasing usage. In this process we also discuss and present techniques that were used, how to use them and their benefits, to help us reach our goal. / ”Home automation” syftar till ett system som låter användaren kontrollera och styra olika apparater i hemmet, ofta sker detta utifrån. Dessa apparater inkluderar, men är inte begränsade till ljusbrytare, termostater, termometrar, persienner eller klimatanläggningar. Potentialen för ett sådant system är enormt då antalet apparater som skulle kunna övervakas med endast minimal och billig extra hårdvara är stort. Många av dessa apparater kan dra nytta av att vara ansluten till ett system som gör det möjligt för ägaren att hantera och styra enheter i deras hem. Antalet apparater är därför mångdubbelt fler än antalet hem som är kopplade till systemet. Det finns flera system på marknaden som ger användaren ett sätt att övervaka och styra en hemmiljö, men dessa system är ofta låsta och stödjer bara specifika enheter. Genom att införa en öppen plattform för allmänheten som inte är bunden till något system, kan vi tillåta att fler enheter kan integreras i hemmet och bidra till ytterligare utveckling av smartare hem. Målet med detta projekt var att skapa en skalbar öppen plattform med möjlighet till asynkron uppdatering. Detta har gjorts genom att implementera flera logiska delar för att förse användaren med ett webbgränssnitt och för att tillåta oss hantera kommunikation och lagring av data. Alla dessa delar är sammanlänkade för att bilda ett system av servrar som hanterar alla bakgrundsprocesser. Denna avhandling diskuterar och presenterar implementeringar av alla dessa servrar, hur de genomförs, kommunicera med varandra, ger säkra anslutningar och hur de kan skala med ökad användning. I denna process diskuterar och presenterar vi de tekniker som använts, hur man använder dem och deras fördelar.

In this dissertation, we study the verification of concurrent programs written in the programming language Erlang using infinite-state model-checking. Erlang is a widely used, higher order, dynamically typed, call-by-value functional language with algebraic data types and pattern-matching. It is further augmented with support for actor concurrency, i.e. asynchronous message passing and dynamic process creation. With decidable model-checking in mind, we identify actor communicating systems (ACS) as a suitable target model for an abstract interpretation of Erlang. ACS model a dynamic network of finite-state processes that communicate over a fixed, finite number of unordered, unbounded channels. Thanks to being equivalent to Petri nets, ACS enjoy good algorithmic properties. We develop a verification procedure that extracts a sound abstract model, in the form of an ACS, from a given Erlang program; the resulting ACS simulates the operational semantics of the input. Using this abstract model, we can conservatively verify coverability properties of the input program, i.e. a weak form of safety properties, with a Petri net model-checker. We have implemented this procedure in our tool Soter, which is the first sound verification tool for Erlang programs using infinite-state model-checking. In our experiments, we find that Soter is accurate enough to verify a range of interesting and non-trivial benchmarks. Even though ACS coverability is Expspace-complete, Soter's analysis of these verification problems is surprisingly quick. In order to improve the precision of our verification procedure with respect to recursion, we investigate an extension of ACS that allows pushdown processes: asynchronously communicating pushdown systems (ACPS). ACPS that satisfy the empty-stack constraint (a pushdown process may receive only when its stack is empty) are a popular subclass of ACPS with good decision and complexity properties. In the context of Erlang, the empty stack constraint is unfortunately not realistic. We introduce a relaxation of the empty-stack constraint for ACPS called the shaped stack constraint. Stacks that fit the shape constraint may reach arbitrary heights. Further, a process may execute any communication action (be it process creation, message send or retrieval) whether or not its stack is empty. We prove that coverability for shaped ACPS, i.e. ACPS that satisfy the shaped constraint, reduces to the decidable coverability problem for well-structured transition systems (WSTS). Thus, shaped ACPS enable the modelling and verification of a larger class of message passing programs. We establish a close connection between shaped ACPS and a novel extension of Petri nets: nets with nested coloured tokens (NNCT). Tokens in NNCT are of two types: simple and complex. Complex tokens carry an arbitrary number of coloured tokens. The rules of a NNCT can synchronise complex and simple tokens, inject coloured tokens into a complex token, and eject all tokens of a specified set of active colours to predefined places. We show that the coverability problem for NNCT is Tower-complete, a new complexity class for non-elementary decision problems introduced by Schmitz. To prove Tower-membership, we devise a geometrically inspired version of the Rackoff technique, and we obtain Tower-hardness by adapting Stockmeyer's ruler construction to NNCT. To our knowledge, NNCT is the first extension of Petri nets (belonging to the class of nets with an infinite set of token types) that is proven to have primitive recursive coverability. This result implies Tower-completeness of coverability for ACPS that satisfy the shaped stack constraint.