Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS

2013 ◽  
Vol 8 (4) ◽  
pp. 323-339 ◽  
Author(s):  
Elvira Albert ◽  
Frank S. de Boer ◽  
Reiner Hähnle ◽  
Einar Broch Johnsen ◽  
Rudolf Schlatte ◽  
...  
Keyword(s):  
Resource Management ◽  
Real Time ◽  
Formal Modeling ◽  
Industrial Case Study ◽  
Modeling And Analysis

scholarly journals Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using UPPAAL

1997 ◽  
Vol 4 (31) ◽  
Author(s):  
Klaus Havelund ◽  
Arne Skou ◽  
Kim G. Larsen ◽  
Kristian Lund
Keyword(s):  
Software Development ◽  
Real Time ◽  
Real Life ◽  
Automatic Verification ◽  
Formal Modeling ◽  
Industrial Case Study ◽  
Modeling And Analysis ◽  
Audio Video ◽  
Assembler Code

A formal and automatic verification of a real-life protocol is presented. The protocol, about 2800 lines of assembler code, has been used in products from the audio/video company Bang & Olufsen throughout more than a decade, and its purpose<br />is to control the transmission of messages between audio/video components over a single bus. Such communications may collide, and one essential purpose of the protocol is to detect such collisions. The functioning is highly dependent on<br />real-time considerations. Though the protocol was known to be faulty in that messages were lost occasionally, the protocol was too complicated in order for Bang & Olufsen to locate the bug using normal testing. However, using the real-time verification<br />tool UPPAAL, an error trace was automatically generated, which caused the detection of “the error” in the implementation. The error was corrected and the correction was automatically proven correct, again using UPPAAL. A future, and more automated, version of the protocol, where this error is fatal, will incorporate the correction. Hence, this work is an elegant demonstration of how model checking has had an impact on practical software development. The effort of modeling this protocol has in addition generated a number of suggestions for enriching the UPPAAL language. Hence, it’s also an excellent example of the reverse impact.

Formal Modeling of Resource Management for Cloud Architectures: An Industrial Case Study

2012 ◽  
pp. 91-106 ◽  
Author(s):  
Frank S. de Boer ◽  
Reiner Hähnle ◽  
Einar Broch Johnsen ◽  
Rudolf Schlatte ◽  
Peter Y. H. Wong
Keyword(s):  
Resource Management ◽  
Formal Modeling ◽  
Industrial Case Study

scholarly journals Formal Modeling and Analysis of Fairness Characterization of E-Commerce Protocols

2014 ◽  
Vol 2014 ◽  
pp. 1-10
Author(s):  
Chengwei Zhang ◽  
Xiaohong Li ◽  
Jing Hu ◽  
Zhiyong Feng ◽  
Jiaojiao Song
Keyword(s):  
Formal Modeling ◽  
Sufficient Condition ◽  
Formal Approach ◽  
Common Assumption ◽  
Modeling And Analysis ◽  
Verification Method ◽  
Space Model ◽  
The Past

In the past, fairness verification of exchanges between the traders in E-commerce was based on a common assumption, so-called nonrepudiation property, which says that if the parties involved can deny that they have received or sent some information, then the exchanging protocol is unfair. So, the nonrepudiation property is not a sufficient condition. In this paper, we formulate a new notion of fairness verification based on the strand space model and propose a method for fairness verification, which can potentially determine whether evidences have been forged in transactions. We first present an innovative formal approach not to depend on nonrepudiation, and then establish a relative trader model and extend the strand space model in accordance with traders’ behaviors of E-commerce. We present a case study to demonstrate the effectiveness of our verification method.

scholarly journals Dynamic Resource Management of Real-Time Edge Services for Intelligent Vehicular Networks: A Case Study

2019 ◽  
Vol 25 (4) ◽  
pp. 58-61
Author(s):  
Katja Gilly ◽  
Sonja Filiposka ◽  
Salvador Alcaraz Carrasco ◽  
Anastas Mishev
Keyword(s):  
Resource Management ◽  
Real Time ◽  
Vehicular Networks ◽  
Urban Environments ◽  
City Centre ◽  
Time Service ◽  
Dynamic Resource Management ◽  
Dynamic Resource ◽  
Multi Access

The Internet of Vehicles requires high bandwidth and low latency services to unleash the potential of fully connected vehicles. Thus, the offloading proposals that successfully manage massive real-time service requests from vehicle nodes are needed. In this paper, we analyse the dynamic resource management for intelligent vehicular networks based on Multi-access Edge Computing architecture services. Using a combination of CloudSim and SUMO simulators, we present a case study of infotainment services in the city centre of Alicante, in Spain, that shows a high degree of optimality both in service allocation and migration when considering dense urban environments.

Sign in / Sign up

Export Citation Format

Share Document