Rigorous development of safety-critical systems

Nowadays, computer-based systems tend to become more complex and control increasingly critical functions affecting different areas of human activities. Failures of such systems might result in loss of human lives as well as significant damage to the environment. Therefore, their safety needs to be ensured. However, the development of safety-critical systems is not a trivial exercise. Hence, to preclude design faults and guarantee the desired behaviour, different industrial standards prescribe the use of rigorous techniques for development and verification of such systems. The more critical the system is, the more rigorous approach should be undertaken. To ensure safety of a critical computer-based system, satisfaction of the safety requirements imposed on this system should be demonstrated. This task involves a number of activities. In particular, a set of the safety requirements is usually derived by conducting various safety analysis techniques. Strong assurance that the system satisfies the safety requirements can be provided by formal methods, i.e., mathematically-based techniques. At the same time, the evidence that the system under consideration meets the imposed safety requirements might be demonstrated by constructing safety cases. However, the overall safety assurance process of critical computerbased systems remains insufficiently defined due to the following reasons. Firstly, there are semantic differences between safety requirements and formal models. Informally represented safety requirements should be translated into the underlying formal language to enable further veri cation. Secondly, the development of formal models of complex systems can be labour-intensive and time consuming. Thirdly, there are only a few well-defined methods for integration of formal verification results into safety cases. This thesis proposes an integrated approach to the rigorous development and verification of safety-critical systems that (1) facilitates elicitation of safety requirements and their incorporation into formal models, (2) simplifies formal modelling and verification by proposing specification and refinement patterns, and (3) assists in the construction of safety cases from the artefacts generated by formal reasoning. Our chosen formal framework is Event-B. It allows us to tackle the complexity of safety-critical systems as well as to structure safety requirements by applying abstraction and stepwise refinement. The Rodin platform, a tool supporting Event-B, assists in automatic model transformations and proof-based verification of the desired system properties. The proposed approach has been validated by several case studies from different application domains.

Gearing Towards Omnichannel Grocery Retail Through Business Model Innovation

Technological innovations and the advent of digitalization have led retail business into one of its biggest transformations of all time. Consumer behaviour has changed rapidly and the customers are ever more powerful, demanding, tech-savvy and moving on various plat-forms. These attributes will continue to drive the development and robustly restructure the architecture of value creation in the retail business. The largest retail category, grocery yet awaits for a real disruption, but the signals for major change are already on the horizon. The first wave of online grocery retail was introduced in the mid 1990’s and it throve until millennium. Many overreactions, heavy investments and the burst IT-bubble almost stag-nated the whole industry for a long period of time. The second wave started with a venge-ance around 2010. Some research was carried out during the first wave from a single-viewpoint of online grocery retail, but without a comprehensive approach to online-offline business model integration. Now the accelerating growth of e-business has initiated an increased interest to examine the transformation from traditional business models towards e-business models and their integration on the companies’ traditional business models. This research strove to examine how can we recognize and analyze how digitalization and online channels are affecting the business models of grocery retail, by using business mod-el canvas as an analysis tool. Furthermore business model innovation and omnichannel retail were presented and suggested as potential solutions for these changes. 21 experts in online grocery industry were being interviewed. The thoughts of the informants were being qualitatively analysed by using an analysis tool called the business model canvas. The aim of this research was to portray a holistic view on the Omnichannel grocery retail business model, and the value chain, in which the case company Arina along with its partners are operating. The key conclusions exhibited that online grocery retail business model is not an alterna-tive model nor a substitute for the traditional grocery retail business model, though all of the business model elements are to some extent affected by it, but rather a complementary business model that should be integrated into the prevailing, conventional grocery retail business model. A set of business model elements, such as value proposition and distribu-tion channels were recognized as the most important ones and sources of innovation within these components were being illustrated. Segments for online grocery retail were empiri-cally established as polarized niche markets in contrast of the segmented mass-market of the conventional grocery retail. Business model innovation was proven to be a considera-ble method and a conceptual framework, by which to come across with new value proposi-tions that create competitive advantage for the company in the contemporary, changing business environment. Arina as a retailer can be considered as a industry model innovator, since it has initiated an entire industry in its market area, where other players have later on embarked on, and in which the contributors of the value chain, such as Posti depend on it to a great extent. Consumer behaviour clearly affects and appears everywhere in the digi-talized grocery trade and it drives customers to multiple platforms where retailers need to be present. Omnichannel retail business model was suggested to be the solution, in which the new technologies are being utilized, contemporary consumer behaviour is embedded in decision-making and all of the segments and their value propositions are being served seamlessly across the channels.