About: Formal Verification of Interoperability Between Future Network Architectures Using Alloy

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Formal Verification of Interoperability Between Future Network Architectures Using Alloy Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : wasabi.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	Formal Verification of Interoperability Between Future Network Architectures Using Alloy
Creator	Chen, Jiachen Jahanian, Mohammad Ramakrishnan, K
topic	covid:eec6907f57648072bf02622a2e13dea97fd012eb#this
Source	PMC
abstract	The Internet is composed of many interconnected, interoperating networks. With the recent advances in Future Internet design, multiple new network architectures, especially Information-Centric Networks (ICN) have emerged. Given the ubiquity of networks based on the Internet Protocol (IP), it is likely that we will have a number of different interconnecting network domains with different architectures, including ICNs. Their interoperability is important, but at the same time difficult to prove. A formal tool can be helpful for such analysis. ICNs have a number of unique characteristics, warranting formal analysis, establishing properties that go beyond, and are different from, what have been used in the state-of-the-art because ICN operates at the level of content names rather than node addresses. We need to focus on node-to-content reachability, rather than node-to-node reachability. In this paper, we present a formal approach to model and analyze information-centric interoperability (ICI). We use Alloy Analyzer’s model finding approach to verify properties expressed as invariants for information-centric services (both pull and push-based models) including content reachability and returnability. We extend our use of Alloy to model counting, to quantitatively analyze failure and mobility properties. We present a formally-verified ICI framework that allows for seamless interoperation among a multitude of network architectures. We also report on the impact of domain types, routing policies, and binding techniques on the probability of content reachability and returnability, under failures and mobility.
has issue date	2020-04-22(xsd:dateTime)
bibo:doi	10.1007/978-3-030-48077-6_4
has license	no-cc
sha1sum (hex)	eec6907f57648072bf02622a2e13dea97fd012eb
schema:url	https://doi.org/10.1007/978-3-030-48077-6_4
resource representing a document's title	Formal Verification of Interoperability Between Future Network Architectures Using Alloy
has PubMed Central identifier	PMC7242041
schema:publication	Rigorous State-Based Methods
resource representing a document's body	covid:eec6907f57648072bf02622a2e13dea97fd012eb#body_text
is http://vocab.deri.ie/void#inDataset of	proxy:http/ns.inria.fr/covid19/eec6907f57648072bf02622a2e13dea97fd012eb
is schema:about of	named entity 'architectures' named entity 'formal analysis' named entity 'level' named entity 'multitude' named entity 'domain' named entity 'HAVE' named entity 'MOBILITY' named entity 'IMPACT' named entity 'MODELS' named entity 'BEYOND' named entity 'ESTABLISHING' named entity 'TECHNIQUES' named entity 'NAMES' named entity 'BUT' named entity 'INTERNET PROTOCOL' named entity 'NUMBER OF' named entity 'CHARACTERISTICS' named entity 'PULL' named entity 'HELPFUL' named entity 'With' named entity 'invariants' named entity 'Given' named entity 'ICN' named entity 'Alloy' named entity 'time' named entity 'Networks' named entity 'Alloy Analyzer' named entity 'ICI' named entity 'Future Internet' named entity 'Centric' named entity 'ICI' named entity 'interoperability' named entity 'probabilistic analysis' named entity 'interoperability' named entity 'Conjunctive Normal Form' named entity 'IP networks' named entity 'scalability' named entity 'interoperability' named entity 'late binding' named entity 'interoperability' named entity 'meta-model' named entity 'P 2' named entity 'formal model' named entity 'demultiplex' named entity 'ICI' named entity 'late binding' named entity 'publish/subscribe' named entity 'Alloy Analyzer' named entity 'IP addresses' named entity 'Early Binding' named entity 'interoperability' named entity 'information retrieval' named entity 'configuration space' named entity 'Late Binding' named entity 'SAT solvers' named entity 'ICI' named entity 'ICNs' named entity 'data plane' named entity 'interoperability' named entity 'ICI' named entity 'ICI' named entity 'interoperability' named entity 'SAT solver' named entity 'state entries' named entity 'ICI' named entity 'ICI' named entity 'transitive closure' named entity 'source code' named entity 'network topology' named entity 'Google' named entity 'Alloy Analyzer' named entity 'interoperability' named entity 'binary relations' named entity 'CNF' named entity 'Internet interoperability' named entity 'SAT-solving' named entity 'ContentID' named entity 'Reverse Path Forwarding' named entity 'interoperability'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software