scholarly journals Implementation of Taylor models in CORA 2018

10.29007/zzc7 ◽  
2018 ◽  
Author(s):  
Matthias Althoff ◽  
Dmitry Grebenyuk ◽  
Niklas Kochdumper

Tool Presentation: Computing guaranteed bounds of function outputs when their input variables are bounded by intervals is an essential technique for many formal methods. Due to the importance of bounding function outputs, several techniques have been proposed for this problem, such as interval arithmetic, affine arithmetic, and Taylor models. While all methods provide guaranteed bounds, it is typically unknown to a formal verification tool which approach is best suitable for a given problem. For this reason, we present an implementation of the aforementioned techniques in our MATLAB tool CORA so that advantages and disadvantages of different techniques can be quickly explored without hav- ing to compile code. In this work we present the implementation of Taylor models and affine arithmetic; our interval arithmetic implementation has already been published. We evaluate the performance of our implementation using a set of benchmarks against Flow* and INTLAB. To the best of our knowledge, we have also evaluated for the first time how a combination of interval arithmetic and Taylor models performs: our results indicate that this combination is faster and more accurate than only using Taylor models.

2016 ◽  
Vol 138 (4) ◽  
Author(s):  
Shaobo Wang ◽  
Xiangyun Qing

Uncertainty is ubiquitous throughout engineering design processes. Robust optimization (RO) aims to find optimal solutions that are relatively insensitive to input uncertainty. In this paper, a new approach is presented for single-objective RO problems with an objective function and constraints that are continuous and differentiable. Both the design variables and parameters with interval uncertainties are represented as affine forms. A mixed interval arithmetic (IA)/affine arithmetic (AA) model is subsequently utilized in order to obtain affine approximations for the objective and feasibility robustness constraint functions. Consequently, the RO problem is converted to a deterministic problem, by bounding all constraints. Finally, nonlinear optimization solvers are applied to obtain a robust optimal solution for the deterministic optimization problem. Some numerical and engineering examples are presented in order to demonstrate the advantages and disadvantages of the proposed approach. The main advantage of the proposed approach lies in the simplicity of the conversion from a nonlinear RO problem with interval uncertainty to a deterministic single-looped optimization problem. Although this approach cannot be applied to problems with black-box models, it requires a minimal use of IA/AA computation and applies some widely used advanced solvers to single-looped optimization problems, making it more suitable for applications in engineering fields.


2011 ◽  
Vol 11 (1) ◽  
pp. 155-176 ◽  
Author(s):  
Minna Kimpimäki

AbstractIn June 2010, a Rwandan citizen, Francois Bazaramba, was sentenced in a Finnish court of first instance, to life imprisonment for acts of genocide committed in Rwanda in 1994. This was the first time that the provisions of Finnish law dealing with genocide had ever been applied in a court. This article examines the details of this case, as well as the Finnish legislation on genocide, jurisdiction and extradition. Many of the questions considered in this article are not only typical for Finland, but have a more general bearing as well. For instance, the issues relating to the transfer or extradition of fugitives to Rwanda have recently been considered in several national and international jurisdictions. A trial conducted in a national court on the basis of universal jurisdiction reveals in a concrete way the advantages and disadvantages of this form of prosecution.


Molecules ◽  
2021 ◽  
Vol 26 (9) ◽  
pp. 2530
Author(s):  
Anton Budeev ◽  
Grigory Kantin ◽  
Dmitry Dar’in ◽  
Mikhail Krasavin

Diazocarbonyl compounds have found numerous applications in many areas of chemistry. Among the most developed fields of diazo chemistry is the preparation of azoles from diazo compounds. This approach represents a useful alternative to more conventional methods of the synthesis of azoles. A comprehensive review on the preparation of various azoles (oxazoles, thiazoles, imidazoles, pyrazoles, triazoles, and tetrazoles) from diazocarbonyl and related compounds is presented for the first time along with discussion of advantages and disadvantages of «diazo» approaches to azoles.


2017 ◽  
Vol 38 (3) ◽  
pp. 351-375 ◽  
Author(s):  
Salah Imam ◽  
David A Coley ◽  
Ian Walker

One of the most discussed issues in the design community is the performance gap. In this research, we investigate for the first time whether part of the gap might be caused by the modelling literacy of design teams. A total of 108 building modellers were asked to comment on the importance of obtaining and using accurate values for 21 common modelling input variables, from U-values to occupancy schedules when using dynamic simulation to estimate annual energy demand. The questioning was based on a real building for which high-resolution energy, occupancy and temperature data were recorded. A sensitivity analysis was then conducted using a model of the building (based on the measured data) by perturbing one parameter in each simulation. The effect of each perturbation on the annual energy consumption given by the model was found and a ranked list generated. The order of this list was then compared to that given by the modellers for the same changes in the parameters. A correlation analysis indicated little correlation between which variables were thought to be important by the modellers and which proved to be objectively important. k-means cluster analysis identified subgroups of modellers and showed that 25% of the people tested were making judgements that appeared worse than a person responding at random. Follow-up checks showed that higher level qualifications, or having many years of experience in modelling, did not improve the accuracy of people’s predictions. In addition, there was no correlation between modellers, with many ranking some parameters as important that others thought irrelevant. Using a three-part definition of literacy, it is concluded that this sample of modellers, and by implication the population of building modellers, cannot be considered modelling literate. This indicates a new cause of the performance gap. The results suggest a need and an opportunity for both industry and universities to increase their efforts with respect to building physics education, and if this is done, a part of the performance gap could be rapidly closed. Practical application: In any commercial simulation, the modeller will have to decide which parameters must be included and which might be ignored due to lack of time and/or data, and how much any approximations might perturb the results. In this paper, the judgment of 108 modellers was compared against each other. The results show that the internal mental models of thermal modellers disagree with one another, and disagree with the results of a validated thermal model. The lessons learnt will be of great utility to modellers, and those educating the next generation of modellers.


Author(s):  
Shahram Rahimi ◽  
Rishath A. S. Rias ◽  
Elham S. Khorasani

The complexity of designing concurrent and highly-evolving interactive systems has grown to a point where system verification has become a hurdle. Fortunately, formal verification methods have arrived at the right time. They detect errors, inconsistencies and incompleteness at early development stages of a system formally modeled using a formal specification language. -calculus (Milner, 1999) is one such formal language which provides strong mathematical base that can be used for verifying system specifications. But manually verifying the specifications of concurrent systems is a very tedious and error-prone work, especially if the specifications are large. Consequently, an automated verification tool would be essential for efficient system design and development. In addition, formal verification tools are vital ingredient to fully harness the potential of component-based software composition. The authors developed such an automated verification tool which is highly portable and seamlessly integrates with the visualization, reduction and performance evaluation tools introduced (Ahmad & Rahimi, 2008; Rahimi, 2006; Rahimi et al., 2001, 2008) to provide a comprehensive tool for designing and analyzing multi process/agent systems. Open-Bisimulation (Sangiorgi, 1996) concept is utilized as the theoretical base for the design and implementation of the tool which incorporates an expert system implemented in Java Expert System Shell (JESS) (Friedman-Hill, 2003).


2013 ◽  
Vol 7 (2) ◽  
pp. 57-85
Author(s):  
Khaoula Marzouki ◽  
Amira Radhouani ◽  
Narjes Ben Rajeb

Electronic voting protocols have many advantages over traditional voting but they are complex and subject to many kinds of attacks. Therefore, the use of formal verification methods is crucial to ensure some security properties. We propose to model a recent protocol of remote electronic voting in the applied Pi-calculus. We focalized on some security properties such as fairness which expresses the impossibility of obtaining partial results, eligibility which requires that only legitimate voters can vote, coercion resistance which ensures that no voter may vote under pressure, and verifiability which supposes that anyone can verify the accuracy of the final result. We proved either manually or using the automated verification tool ProVerif that the protocol satisfies these security properties.


Author(s):  
Luciana Brasil Rebelo dos Santos ◽  
Eduardo Rohde Eras ◽  
Valdivino Alexandre de Santiago Júnior ◽  
Nandamudi Lankalapalli Vijaykumar

2019 ◽  
Vol 159 ◽  
pp. 1431-1438
Author(s):  
Giovanni Capobianco ◽  
Umberto Di Giacomo ◽  
Francesco Mercaldo ◽  
Antonella Santone

Sign in / Sign up

Export Citation Format

Share Document