1,721,022 research outputs found
Cloud Deployment Tradeoffs for the Analysis of Spatially Distributed Internet of Things Systems
No full textInternet-enabled devices operating in the physical world are increasingly integrated in modern distributed systems. We focus on systems where the dynamics of spatial distribution is crucial; in such cases, devices may need to carry out complex computations (e.g., analyses) to check satisfaction of spatial requirements. The requirements are partly global - as the overall system should achieve certain goals - and partly individual, as each entity may have different goals. Assurance may be achieved by keeping a model of the system at runtime, monitoring events that lead to changes in the spatial environment, and performing requirements analysis. However, computationally intensive runtime spatial analysis cannot be supported by resource-constrained devices and may be offloaded to the cloud. In such a scenario, multiple challenges arise regarding resource allocation, cost, performance, among other dimensions. In particular, when the workload is unknown at the system's design time, it may be difficult to guarantee application-service-level agreements, e.g., on response times. To address and reason on these challenges, we first instantiate complex computations as microservices and integrate them to an IoT-cloud architecture. Then, we propose alternative cloud deployments for such an architecture - based on virtual machines, containers, and the recent Functions-as-a-Service paradigm. Finally, we assess the feasibility and tradeoffs of the different deployments in terms of scalability, performance, cost, resource utilization, and more. We adopt a workload scenario from a known dataset of taxis roaming in Beijing, and we derive other workloads to represent unexpected request peaks and troughs. The approach may be replicated in the design process of similar classes of spatially distributed IoT systems.Fil: Tsigkanos, Christos. Vienna University of Technology; AustriaFil: Garriga, Martín. Universidad Nacional del Comahue; Argentina. Consejo Nacional de Investigaciones Científicas y Técnicas. Centro Científico Tecnológico Conicet - Patagonia Norte; ArgentinaFil: Baresi, Luciano. Politecnico di Milano; ItaliaFil: Ghezzi, Carlo. Politecnico di Milano; Itali
Security requirements, modelling and analysis in a courthouse case study
Full text linkLAUREA MAGISTRALENel settore delle costruzioni, i modelli di informazione dell’edificio (BIM) rappresentano lo standard per la specifica di informazioni complesse riguardanti la costruzione delle infrastrutture. Utilizzando il Palazzo di Giustizia di Pavia come caso di studio e considerando le problematiche di sicurezza di questo particolare dominio, seguiamo i principi dell’ingegneria del software per consentire concretamente l’analisi dei requisiti di sicurezza sul progetto dell’edificio. Inizialmente viene affrontata la problematica della raccolta dei requisiti, a cui segue l’analisi dei requisiti. In tale dominio possono essere presi in considerazione requisiti riguardanti strutture statiche presenti nel progetto del Palazzo di Giustizia oppure valutare complessi scenari che evolvono in comportamenti dinamici dei beni e delle persone che si trovano all’interno. Vista la disponibilità delle descrizioni BIM dello spazio fisico del tribunale che compongono il dominio, siamo andati ad utilizzarle come fondamenta, allo scopo di ottenere modelli sensibili all’analisi attraverso l’impiego di tecniche per la trasformazione tra modelli. In particolare sfruttiamo la struttura presente nelle descrizioni Industry Foundation Classes e andiamo a generare un grafo rappresentante la topologia delle entità importanti presenti nel progetto degli spazi fisici del Palazzo di Giustizia. Concludiamo mostrando le analisi effettuate mediante strumenti esterni sui modelli ottenuti di requisiti generali, presi ad esempio, sia di natura fisica che dinamica.In the construction industry, Building Information Models (BIM) are the standard for specifying complex information about building infrastructures. Using the courthouse of Pavia as a case study, and considering security concerns of this particular domain, we follow software engineering principles to concretely enable analysis of security requirements of the building design. The problem of security requirements elicitation is initially addressed, followed by requirements analysis. Requirements in such a domain can predicate about static structures inherent in the courthouse physical space design, or reason about complex scenarios that involve dynamic behaviour of assets or people inhabiting it. Since BIM descriptions of the courthouse physical space were available for the domain, we utilize those as the foundation to obtain models amenable for analysis through model-to-model transformation techniques. In particular, we exploit structure in Industry Foundation Classes descriptions and generate a graph representing topology of important entities in the courthouse physical space design. We conclude by showcasing analysis over obtained models of generic example requirements of both static and dynamic nature, through external tools
On model-driven design of city spaces. A bidirectional transformations approach to city spaces design and operations
Full text linkLAUREA MAGISTRALELa proliferazione di ambienti intelligenti nella società contemporanea ha fatto sorgere l'esigenza di strumenti di analisi che ne supportino un'ingegnerizzazione sistematica.
Il progresso tecnologico che ha dato forma a questa realtà ha creato un mondo in cui elementi fisici e computazionali interagiscono e possono esibire comportamenti complessi, come quelli di \emph{smart city} e \emph{smart building}. Le tecniche basate su modelli si sono affermate come un metodo per facilitarne lo sviluppo e l'analisi.
Nello spirito di tali approcci, il modello dello spazio fisico ereditato dall'architettura e dall'ingegneria civile è trasformato in un modello \emph{analizzabile}, all'interno del quale vengono innestate funzionalità intelligenti.
Tali modelli possono allora essere analizzati formalmente per valutare il design di un sistema composito.
Tra le rappresentazioni specifiche di dominio, questa tesi si focalizza su modelli dello spazio fisico specificati nel linguaggio standard CityGML e su come questi possano essere trasformati in modelli apprezzabili da un punto di vista analitico. Si vuole mostrare inoltre, come tali modelli possano essere sincronizzati automaticamente con quelli originali, qualora si verificassero aggiornamenti in ambo le parti.
Come modelli \emph{analizzabili}, abbiamo considerato gli spazi cyber-fisici, una rappresentazione che combina elementi fisici e computazionali.
Presentiamo il problema in un'impostazione formale, definiamo la relazione di consistenza tra due tipi di modelli e presentiamo un software per la trasformazione automatica bidirezionale tra modelli CityGML e spazi cyber-fisici. Esibiamo, infine, la trasformazione su dei modelli di città reali e concludiamo con una discussione sulle possibili limitazioni ed estensioni.The proliferation of smart environments in contemporary societies has led to demands for analysis facilities to support their systematic engineering.
Technological advancements shaping such environments have led to
a world in which physical and computational elements interact and may exhibit complex behavior, such as within smart buildings and smart cities. Model-based techniques have been proposed to ease development and analysis.
In such an approach, the model of physical space coming from architecture and civil engineering
disciplines is transformed into an analyzable model upon which
smart functionalities can be embedded.
Such models can then be formally analyzed to assess a composite system design.
Among domain-specific descriptions, this thesis focuses on how a model of physical space specified in the CityGML standard language can be transformed into a model amenable
to analysis and how the two models can be automatically kept
in sync after possible changes.
The analyzable model is a cyber-physical space, a representation combining physical and computational elements.
We discuss the problem in a formal setting and define a consistency
relation between the two types of models, and present a software tool
for automatic bidirectional transformations between CityGML models
and cyber-physical spaces. We showcase transformations over
real city models and conclude with a discussion on limitations and possible extensions
HarVey. On runtime veri cation of cyber-physical spaces
No full textLAUREA MAGISTRALEGli spazi cyber-fisici sono ambienti complessi, con capacità di calcolo e comunicazione integrate, dove non c'è un chiaro confine tra il mondo digitale e quello fisico. Le smart cities o gli smart buildings sono un classico esempio di spazi cyber-physici. In questi sistemi, dove agli utenti vengono forniti servizi digitali grazie a tecnologie come l'Internet of Things o il Cloud computing, è necessario garantire che il servizio sia effettivamente erogato nella maniera prestabilita, evitando comportamenti indesiderati che potrebbero portare ad una violazione dei requisiti del sistema stesso. Spesso, questi comportamenti non possono essere verificati in fase di design del sistema, per esempio per via della complessità del sistema stesso o l'elevato numero di agenti che interagiscono con esso. Servono perciò delle tecniche applicate in fase di esecuzione del sistema per monitorarne il comportamento, che solitamente consentono di esprimere proprietà del sistema in uno specifico linguaggio formale, oltre che assicurare che il sistema non violi tali proprietà.
Questa tesi ha come obiettivo la definizione di un framework per la verifica a runtime di uno spazio cyber-fisico, in grado di monitorarne propriet\'{a} comportamentali. Gli spazi cyber-physici sono modellizzati attraverso l'uso di grafi bipartiti, mentre le propriet\'{a} sono espresse in logica temporale metrica del primo ordine (MFOTL), che usando grafi bipartiti al suo interno consente di descrivere sia propriet\'{a} strutturali che propriet\'{a} temporali.
Il linguaggio risultante pu\`{o} essere usato per monitorare ambienti cyber-fisici complessi, come smart cities o smart buildings. Per la valutazione dei predicati logici e dei grafi bipartiti, sono stati integrati componenti aggiuntivi.
Il framework \`{e} stato valutato usando come caso di studio un systema di bike sharing in una smart city, discutendo l'espressivit\'{a} e la realizzabilit\'{a} del nostro approccio.Cyber-physical spaces are complex environments with embedded computing and communication capabilities, where there's no clear boundary between digital and physical world. Smart cities or smart buildings are common examples of cyber-physical spaces. In such systems, where integrated digital services are provided to users thanks to technologies like the Internet of Things or Cloud computing, we must guarantee that a service is delivered to a user in the intended way, avoiding undesired behaviors that may lead to requirement violations. Often, such behaviors cannot be ensured at design time, e.g. due to the complexity of the system or the high number of agents interacting with it. Thus, techniques situated at runtime to monitor a system's behavior must be considered, which usually enable stating properties of a system in a suitable formal language as well as ensuring that the system does not violate them. This thesis aims at the de nition of a runtime veri cation technical framework able to monitor behavioral properties of cyber-physical spaces. Cyberphysical spaces are modelled using bigraphs, a formalism for structures in ubiquitous computing, while properties are expressed using Metric First Order Temporal Logic (MFOTL) over parametric bigraphical patterns, capturing both structural and temporal properties of a system. The resulting language can be used to monitor complex cyber-physical environments such as smart cities or buildings. For the evaluation of MFOTL predicates and bigraphical patterns, external tools are integrated. We evaluate our framework using a case study of a bike sharing system in a smart city, and discuss preliminary results regarding expressiveness and realizability of our approach
Dynamic Cyber-Physical Spaces
No full textComputing and communication capabilities are increasingly being embedded into physical spaces blurring the boundary between computational and physical worlds; typically, this is the case in modern cyber-physical or internet-of-things (IoT) systems. Conceptually, such composite environments can be abstracted into a topological model where computational and physical entities are connected in a graph structure, yielding a cyber-physical space. Like any other software-intensive system, such a space is highly dynamic and typically undergoes continuous change - it is evolving. This brings a manifold of challenges as dynamics may affect e.g. safety, security, or reliability requirements. Modelling space and its dynamics as well as supporting formal reasoning about various properties of an evolving space, are crucial prerequisites for engineering dependable space-intensive systems, e.g. to assure requirements satisfaction or to trigger correct adaptation.
This talk will show an avenue for research which can be characterized as rethinking spatial environments from a software engineering perspective - in both design and operation aspects. Regarding design, we will see how domain descriptions can give rise to models amenable to automated analyses of dynamic behaviours on spaces populated with humans, robots, or mobile devices. Analysis amounts to assessing if some collective behaviour that is highly space-dependent, violates certain requirements that the overall system should exhibit. Regarding runtime, we will consider supporting analyses on the cloud on behalf of resource-constrained and spatially-distributed IoT devices. We will discuss how spatial verification processes can be integrated in the service layer of an IoT-cloud architecture based on microservices, and what tradeoffs emerge across different deployment options
Modelling and verification of evolving cyber-physical spaces
No full textLa separazione tra mondo fisico ed elettronico è in costante riduzione. Dispositivi con capacità computazionale sono sempre maggiormente presenti negli spazi fisici riducendo le barriere tra uomo e macchina. Tipicamente, questo avviene nei moderni sistemi cyber-fisici, come smart building e city. Questi ambienti, indicati nel seguito come spazi cyber-fisici (CPSp), possono essere astratti mediante modelli topologici, dove entità computazionali e fisiche sono connesse per mezzo di strutture matematiche, come ad esempio grafi. Come tutti i sistemi software, gli spazi cyber-fisici sono estremamente dinamici e tipicamente sono soggetti a continui cambiamenti. Questa costante evoluzione comporta una serie di sfide riguardanti la sicurezza e l’affidabilità del sistema. Modellizzare formalmente lo spazio nel quale un’applicazione è in esecuzione e la sua evoluzione, fornendo dei meccanismi che consentano di ragionare sulle proprietà del sistema a fronte dei vari cambia- menti, è un prerequisito essenziale per progettare degli spazi cyber-fisici che soddisfino i loro requisiti a fronte dei cambiamenti che avvengono nello spazio. Questa tesi propone una metodologia e un framework che supportano la modellizzazione di un sistema cyber-fisico e della sua evoluzione e l’analisi delle sue proprietà spazio-temporali. Vengono utilizzati bigraph come formalismo per modellizzare i CPSp e i suoi cambiamenti. Il sistema così generato è un sistema reattivo specificato per mezzo di regole di riscrittura che modellizzano l’evoluzione del sistema in base a condizioni che possono verificarsi localmente e globalmente nel sistema. Il meccanismo di reasoning consente di selezionare le funzionalità del sistema utilizzando un algoritmo di model checking per verificare il soddisfacimento di un insieme di requisiti specificati per mezzo di appropriati formalismi logici. La metodologia proposta consente di progettare un sistema, consentendo la modifica dei meccanismi di sicurezza a run time e la verifica dei requisiti del sistema durante tutto il processo di design.Computing and communication capabilities are increasingly being embedded into physical spaces thus blurring the boundary between computational and physical worlds; typically, this is the case in modern cyber-physical systems, like smart buildings or smart cities. Conceptually, such composite environments, hereafter called cyber-physical spaces (CPSp), can be abstracted into a topological model where computational and physical entities are connected in a discrete, graph-like structure. Like any other software-intensive system, a CPSp is highly dynamic and typically undergoes continuous change, a fact we emphasise by the notion of evolving CPSp. This brings a manifold of challenges as dynamics may affect safety, security, or reliability requirements of the overall space-dependent software system. Formally modelling space and its dynamics as well as supporting reasoning about various properties of evolving space, is a crucial prerequisite for engineering dependable evolving CPSp, e.g. to assure requirements satisfaction or to trigger correct adaptation. Thus, we propose a methodology and technical framework which support modelling of evolving cyber-physical spaces and reasoning about their spatio-temporal properties. We utilise bigraphs as a formalism for modelling CPSp as well as primitives of change, giving rise to a reactive system consisting of rewriting rules with both local and global application conditions. Formal reasoning facilities feature adopting logic-based specification of properties and according model checking procedures, in both spatial and temporal fragments. Utilising these foundations, we consider systematically engineering systems and support both verification of requirements in early stages of design and devising adaptive security behaviours at run time.DIPARTIMENTO DI ELETTRONICA, INFORMAZIONE E BIOINGEGNERIAComputer Science and Engineering29BARESI, LUCIANOBONARINI, ANDRE
Going Beyond Counting First Authors in Author Co-citation Analysis
Full text linkThe present study examines one of the fundamental aspects of author co-citation analysis (ACA) - the way co-citation
counts are defined. Co-citation counting provides the data on which all subsequent statistical analyses and mappings
are based, and we compare ACA results based on two different types of co-citation counting - the traditional type that
only counts the first one among a cited work's authors on the one hand and a non-traditional type that takes into
account the first 5 authors of a cited work on the other hand. Results indicate that the picture produced through this non-traditional author co-citation counting contains more coherent author groups and is therefore considerably clearer. However, this picture represents fewer specialties in the research field being studied than that produced through the traditional first-author co-citation counting when the same number of top-ranked authors is selected and analyzed. Reasons for these effects are discussed
- …
