Abstract
The IEC 61499 standard proposes an event driven execution model for component based (in terms of Function Blocks), distributed industrial automation applications. However, the standard provides only an informal execution semantics, thus in consequence behavior and correctness relies on the design decisions made by the tool vendor. In this paper we present the formalization of a subset of the IEC 61499 standard in order to provide an underpinning for the static verification of Function Block models by means of deductive reasoning. Specifically, we contribute by addressing verification at the component, algorithm, and ECC levels. From Function Block descriptions, enriched with formal contracts, we show that correctness of component compositions, as well as functional and transitional behavior can be ensured. Feasibility of the approach is demonstrated by manually encoding a set of representative use-cases in WhyML, for which the verification conditions are automatically derived (through the Why3 platform) and discharged (using automatic SMT-based solvers). Furthermore, we discuss opportunities and challenges towards deriving certified executables for IEC 61499 models. © 2016 IEEE.

Abstract

Abstract
Nowadays, the prevalence of computing systems in our lives is so ubiquitous that it would not be far-fetched to state that we live in a cyber-physical world dominated by computer systems. These systems demand for more and more computational performance to process large amounts of data from multiple data sources, some of them with guaranteed processing response times. In other words, systems are required to deliver their results within pre-defined (and sometimes extremely short) time bounds. Examples can be found for instance in intelligent transportation systems for fuel consumption reduction in cities or railway, or autonomous driving of vehicles. To cope with such performance requirements, chip designers produced chips with dozens or hundreds of cores, interconnected with complex networks on chip. Unfortunately, the parallelization of the computing activities brings many challenges, among which how to provide timing guarantees, as the timing behaviour of the system running within a many-core processor depends on interactions on shared resources that are most of the time not know by the system designer. P-SOCRATES (Parallel Software Framework for Time-Critical Many-core Systems) is an FP7 European project, which developed a novel methodology to facilitate the deployment of standardized parallel architectures for real-time applications. This methodology was implemented (based on existent models and components) to provide an integrated software development kit, the UpScale SDK, to fully exploit the huge performance opportunities brought by the most advanced many-core processors, whilst ensuring a predictable performance and maintaining (or even reducing) development costs of applications. The presentation will provide an overview of the UpScale SDK, its underlying methodology, and the results of its application on relevant industrial use-cases.

Abstract

Abstract

Abstract
Smart governance is one of the characteristics of smart cities, having its roots in e-government, in the principles of good governance, and in the assumptions of citizens' participation and involvement in public decision-making. This chapter aims to answer the question: “What smart governance practices are being implemented in smart cities” through an extensive literature review in the areas of e-government, good governance, smart cities and smart governance, and content analysis of the websites of seven smart cities: Amsterdam, Barcelona, Copenhagen, Lisbon, Manchester, Singapore, and Stockholm. The objective was to identify the presence of factors related with e-participation; e-services; and public administration functioning on the cities' websites. The chapter ends with directions for future research and the conclusion that all the smart cities analyzed presented some factors related with smart governance, but with different levels of development and application.