Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTowards Enabling Overture as a Platform for Formal Notation IDEs
58
0
0.0
(
0
)
Added by
EPTCS
Publication date
2015
fields
Informatics Engineering
and research's language is
English
Authors
Luis Diogo Couto
Ask ChatGPT about the research
No Arabic abstract
Formal Methods tools will never have as many users as tools for popular programming languages and so the effort spent on constructing Integrated Development Environments (IDEs) will be orders of magnitudes lower than that of programming languages such as Java. This means newcomers to formal methods do not get the same user experience as with their favourite programming IDE. In order to improve this situation it is essential that efforts are combined so it is possible to reuse common features and thus not start from scratch every time. This paper presents the Overture platform where such a reuse philosophy is present. We give an overview of the platform itself as well as the extensibility principles that enable much of the reuse. The paper also contains several examples platform extensions, both in the form of new features and a new IDE supporting a new language.
rate research
Read More
Blockchain is an innovative distributed ledger technology which has attracted a wide range of interests for building the next generation of applications to address lack-of-trust issues in business. Blockchain as a service (BaaS) is a promising solution to improve the productivity of blockchain application development. However, existing BaaS deployment solutions are mostly vendor-locked: they are either bound to a cloud provider or a blockchain platform. In addition to deployment, design and implementation of blockchain-based applications is a hard task requiring deep expertise. Therefore, this paper presents a unified blockchain as a service platform (uBaaS) to support both design and deployment of blockchain-based applications. The services in uBaaS include deployment as a service, design pattern as a service and auxiliary services. In uBaaS, deployment as a service is platform agnostic, which can avoid lock-in to specific cloud platforms, while design pattern as a service applies design patterns for data management and smart contract design to address the scalability and security issues of blockchain. The proposed solutions are evaluated using a real-world quality tracing use case in terms of feasibility and scalability.
This paper reports on the results of the French ANR IMPEX research project dealing with making explicit domain knowledge in design models. Ontologies are formalised as theories with sets, axioms, theorems and reasoning rules. They are integrated to design models through an annotation mechanism. Event-B has been chosen as the ground formal modelling technique for all our developments. In this paper, we particularly describe how ontologies are formalised as Event-B theories.
In this paper we describe the architecture of a Platform as a Service (PaaS) oriented to computing and data analysis. In order to clarify the choices we made, we explain the features using practical examples, applied to several known usage patterns in the area of HEP computing. The proposed architecture is devised to provide researchers with a unified view of distributed computing infrastructures, focusing in facilitating seamless access. In this respect the Platform is able to profit from the most recent developments for computing and processing large amounts of data, and to exploit current storage and preservation technologies, with the appropriate mechanisms to ensure security and privacy.
Blockchain has attracted a broad range of interests from start-ups, enterprises and governments to build next generation applications in a decentralized manner. Similar to cloud platforms, a single blockchain-based system may need to serve multiple tenants simultaneously. However, design of multi-tenant blockchain-based systems is challenging to architects in terms of data and performance isolation, as well as scalability. First, tenants must not be able to read other tenants data and tenants with potentially higher workload should not affect read/write performance of other tenants. Second, multi-tenant blockchain-based systems usually require both scalability for each individual tenant and scalability with number of tenants. Therefore, in this paper, we propose a scalable platform architecture for multi-tenant blockchain-based systems to ensure data integrity while maintaining data privacy and performance isolation. In the proposed architecture, each tenant has an individual permissioned blockchain to maintain their own data and smart contracts. All tenant chains are anchored into a main chain, in a way that minimizes cost and load overheads. The proposed architecture has been implemented in a proof-of-concept prototype with our industry partner, Laava ID Pty Ltd (Laava). We evaluate our proposal in a three-fold way: fulfilment of the identified requirements, qualitative comparison with design alternatives, and quantitative analysis. The evaluation results show that the proposed architecture can achieve data integrity, performance isolation, data privacy, configuration flexibility, availability, cost efficiency and scalability.
In modern cloud-based architectures, containers play a central role: they provide powerful isolation mechanisms such that developers can focus on the logic and dependencies of applications while system administrators can focus on deployment and management issue. In this work, we propose a formal model for container-based systems, using the framework of Bigraphical Reactive Systems (BRSs). We first introduce local directed bigraphs, a graph-based formalism which allows us to deal with localized resources. Then, we define a signature for modelling containers and provide some examples of bigraphs modelling containers. These graphs can be analysed and manipulated using techniques from graph theory: properties about containers can be formalized as properties of the corresponding bigraphic representations. Moreover, it turns out that the composition of containers as performed by e.g. docker-compose, corresponds precisely to the composition of the corresponding bigraphs inside an ``environment bigraph which in turn is obtained directly from the YAML file used to define the composition of containers.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
