Händelser: Data- och informationsteknikhttp://www.chalmers.se/sv/om-chalmers/kalendariumAktuella händelser på Chalmers tekniska högskolaMon, 06 Dec 2021 15:22:36 +0100http://www.chalmers.se/sv/om-chalmers/kalendariumhttps://www.chalmers.se/sv/institutioner/m2/kalendarium/Sidor/Digitalisering-inom-sjöfarten.aspxhttps://www.chalmers.se/sv/institutioner/m2/kalendarium/Sidor/Digitalisering-inom-sj%C3%B6farten.aspxDigitalisering inom sjöfarten<p>Tesla, conference room, Lindholmspiren 5, Navet. Eller online via länk som meddelas efter anmälan.</p><p>​Välkommen till en workshop om digitaliseringen inom sjöfarten</p>​<div>Den tekniska omvandlingen som pågår inom sjöfarten har lett till en decentralisering av kontroll. Som ett resultat av det blir arbetet splittrat när uppgifter fördelas mellan flera mänskliga och artificiella aktörer, på olika platser och i olika organisationer.</div> <div>Målet med den här workshoppen är att diskutera den pågående digitaliseringsprocessen inom sjöfarten och att utforska hur samarbetet förändras när arbetet fördelas mellan människor och autonoma tekniker.</div> <div><br /></div> <div>Workshoppen är ett samarete mellan institutionen för mekanik och maritima vetenskaper på Chalmers och institutionen för tillämpad informationsteknologi på Göteborgs universitet. Värdar för workshoppen är <a href="/sv/personal/Sidor/olle-lindmark.aspx" target="_blank" title="Mer information om Olle Lindmark">Olle Lindmark</a> och <a href="https://www.gu.se/om-universitetet/hitta-person/charlottsellberg" title="Mer information om Charlott Sellberg" target="_blank">Charlott Sellberg</a>.</div> https://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/licentiate-seminar-Niklas-Akerblom.aspxhttps://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/licentiate-seminar-Niklas-Akerblom.aspxNiklas Åkerblom, Data- och informationsteknik<p>Zoom, link above</p><p>​Online learning for energy efficient navigation in stochastic transport networks</p><div><br /></div> <div>Reducing the dependence on fossil fuels in the transport sector is crucial to have a realistic chance of halting climate change. The automotive industry is, therefore, transitioning towards an electrified future at an unprecedented pace. However, in order for electric vehicles to be an attractive alternative to conventional vehicles, some issues, like range anxiety, need to be mitigated. One way to address these problems is by developing more accurate and robust navigation systems for electric vehicles. Furthermore, with highly stochastic and changing traffic conditions, it is useful to continuously update prior knowledge about the traffic environment by gathering data. Passively collecting energy consumption data from vehicles in the traffic network might lead to insufficient information gathered in places where there are few vehicles. Hence, in this thesis, we study the possibility of adapting the routes presented by the navigation system to adequately explore the road network, and properly learn the underlying energy model. <br /></div> <div><br /></div> <div>The first part of the thesis introduces an online machine learning framework for navigation of electric vehicles, with the objective of adaptively and efficiently navigating the vehicle in a stochastic traffic environment. We assume that the road-specific probability distributions of vehicle energy consumption are unknown, and thus, we need to learn their parameters through observations. Furthermore, we take a Bayesian approach and assign prior beliefs to the parameters based on longitudinal vehicle dynamics. We view the task as a combinatorial multi-armed bandit problem, and utilize Bayesian bandit algorithms, such as Thompson Sampling, to address it. We establish theoretical performance guarantees for Thompson Sampling, in the form of upper bounds on the Bayesian regret, on single-agent, multi-agent and batched feedback variants of the problem. To demonstrate the effectiveness of the framework, we perform simulation experiments on various real-life road networks. <br /></div> <div><br /></div> <div>In the second half of the thesis, we extend the online learning framework to find paths which minimize or avoid bottlenecks. Solutions to the online minimax path problem represent risk-averse behaviors, by avoiding road segments with high variance in costs. We derive upper bounds on the Bayesian regret of Thompson Sampling adapted to this problem, by carefully handling the non-linear path cost function. We identify computational tractability issues with the original problem formulation, and propose an alternative approximate objective with an associated algorithm based on Thompson Sampling. Finally, we conduct several experimental studies to evaluate the performance of the approximate algorithm.</div>https://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Thesis-defence-Victor-Lopez-Juan.aspxhttps://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Thesis-defence-Victor-Lopez-Juan.aspxVictor López Juan, Data- och informationsteknik<p>Zoom, link above</p><p>​​Practical Heterogeneous Unification for Dependent Type Checking</p><div><br /></div> <div>Dependent types can specify in detail which inputs to a program are allowed, and how the properties of its output depend on the inputs. A program called the type checker assesses whether a program has a given type, thus detecting situations where the implementation of a program potentially differs from its intended behaviour. When using dependent types, the inputs to a program often occur in the types of other inputs or in the type of the output. The user may omit some of these redundant inputs when calling the program, expecting the type-checker to infer those subterms automatically. <br /></div> <div><br /></div> <div>Some type-checkers restrict the inference of missing subterms to those cases where there is a provably unique solution. This makes the process more predictable, but also limits the situations in which the omitted terms can be inferred; specially when considering that whether a unique solution exists is in general an undecidable problem. This restriction can be made less limiting by giving flexibility to the type-checker regarding the order in which the missing subterms are inferred. The type-checker can then use the information gained by filling in any one subterm in order to infer others, until the whole program has been type-checked. However, this flexibility may in some cases lead to ill-typed subterms being inferred, breaking internal invariants of the type-checker and causing it to crash or loop. The type checker could mitigate this by consistently rechecking the type of each inferred subterm, but this might incur a performance penalty. </div> <div><br /></div> <div>An approach by Gundry and McBride (2012) called twin types has the potential to afford the desired flexibility while preserving well-typedness invariants. However, this method had not yet been tested in a practical setting. In this thesis we streamline the method of twin types in order to ease its practical implementation, justify the correctness of our modifications, and then implement the result in an established dependently-typed language called Agda. We show that our implementation resolves certain existing bugs in Agda while still allowing a wide range of examples to be type-checked, and achieves this without heavily impacting performance. </div>https://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/licentiate-seminar-Ricardo-Diniz-Caldas.aspxhttps://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/licentiate-seminar-Ricardo-Diniz-Caldas.aspxRicardo Diniz Caldas, Data- och informationsteknik<p>Zoom, link above</p><p>​Engineering software for resilient cyber-physical systems</p><div>​​</div> <div>Designing, implementing, and verifying resilient cyber-physical systems is challenging. Resilience is the ability to provide the required capability when facing adversity. Resilient cyber-physical systems should avoid, withstand, recover from, and evolve and adapt to cope with adversity stemming from computation, networking, or physical environment. From the engineering point of view, the usefulness of such systems is hindered by their lack of ability to adapt and overcome unknown stimuli, ever-changing and conflicting objectives, and deprecated internal components. </div> <div><br /></div> <div>Software as a tool for self-management is a key instrument for dealing with uncertainty. Yet, engineering software for resilient cyber-physical systems is hard since the effects of operating under the unknown might emerge during the execution, requesting decision-making at runtime rather than design time. Decision-making at runtime should guarantee the satisfaction of system goals, work efficiently to be effectively used in practice, and guarantee the expected quality. With this in mind, this thesis contributes towards the engineering of software for resilient cyber-physical systems by (i) combining control theory and artificial intelligence for efficient adaptation, (ii) using formal methods for ensuring correctness of control-theoretic software adaptation, and (iii) promoting a language for scenario-based testing autonomous systems. We found that the hybrid approach, combining control theory and artificial intelligence, improves the efficiency of the adaptation mechanism. </div> <div><br /></div> <div>The results shed light on the interplay between control theory and artificial intelligence as fundaments for engineering resilient cyber-physical systems. Yet, incorporating machine learning and control theory introduces non-deterministic autonomic behavior, posing a challenge for the assurance provision for such tools. On the one hand, we found that the use of formal methods helps to build confidence in software-based controllers. On the other hand, large and complex systems place barriers to the usage of formal methods. Thus, we explore the use of testing and specifically scenario-based testing for validating large and complex cyber-physical systems that are required to operate in complex and unpredictable environments, like autonomous vehicles. In a nutshell, this thesis argues in favor of introducing control theory and artificial intelligence in designing and implementing software-based controllers. Also, we exploit formal methods and testing as instruments for verifying and validating cyber-physical systems. </div>