Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems (Tool Demonstration)
74
0
0.0
(
0
)
Added by
Lucas Carvalho Cordeiro
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
An automated counterexample reproducibility tool based on MATLAB is presented, called DSValidator, with the goal of reproducing counterexamples that refute specific properties related to digital systems. We exploit counterexamples generated by the Digital System Verifier (DSVerifier), which is a model checking tool based on satisfiability modulo theories for digital systems. DSValidator reproduces the execution of a digital system, relating its input with the counterexample, in order to establish trust in a verification result. We show that DSValidator can validate a set of intricate counterexamples for digital controllers used in a real quadrotor attitude system within seconds and also expose incorrect verification results in DSVerifier. The resulting toolbox leverages the potential of combining different verification tools for validating digital systems via an exchangeable counterexample format.
rate research
Read More
We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space and accounting for errors due to the digitalization of signals by the controller. Our approach has two stages, leveraging counterexample guided inductive synthesis (CEGIS) and reachability analysis. CEGIS synthesizes a static feedback controller that stabilizes the system under restrictions given by the safety of the reach space. Safety is verified either via BMC or abstract acceleration; if the verification step fails, we refine the controller by generalizing the counterexample. We synthesize stable and safe controllers for intricate physical plant models from the digital control literature.
Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counter-example guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and its rounding errors. We have implemented our new algorithm in a tool called DSSynth, and are able to automatically generate stable controllers for a set of intricate plant models taken from the literature within minutes.
A MATLAB toolbox is presented, with the goal of checking occurrences of design errors typically found in fixed-point digital systems, considering finite word-length effects. In particular, the present toolbox works as a front-end to a recently introduced verification tool, known as Digital-System Verifier, and checks overflow, limit cycle, quantization, stability, and minimum phase errors, in digital systems represented by transfer-function and state-space equations. It provides a command-line version, with simplified access to specific functions, and a graphical-user interface, which was developed as a MATLAB application. The resulting toolbox is important for the verification community, since it shows the applicability of verification to real-world systems.
The advent of the Web brought about major changes in the way people search for jobs and companies look for suitable candidates. As more employers and recruitment firms turn to the Web for job candidate search, an increasing number of people turn to the Web for uploading and creating their online resumes. Resumes are often the first source of information about candidates and also the first item of evaluation in candidate selection. Thus, it is imperative that resumes are complete, free of errors and well-organized. We present an automated resume evaluation tool called CareerMapper. Our tool is designed to conduct a thorough review of a users LinkedIn profile and provide best recommendations for improved online resumes by analyzing a large number of online user profiles.
Asteroseismic observations are crucial to constrain stellar models with precision. Bayesian Estimation of STellar Parameters (BESTP) is a tool that utilizes Bayesian statistics and nested sampling Monte Carlo algorithm to search for the stellar models that best match a given set of classical and asteroseismic constraints from observations. The computation and evaluation of models are efficiently performed in an automated and a multi-threaded way. To illustrate the capabilities of BESTP, we estimate fundamental stellar properties for the Sun and the red-giant star HD 222076. In both cases, we find models that are consistent with the observations. We also evaluate the improvement in the precision of stellar parameters when the oscillation frequencies of individual modes are included as constraints, compared to the case when only the the large frequency separation is included. For the solar case, the uncertainties of estimated masses, radii and ages are reduced by 0.7%, 0.3% and 8% respectively. For HD 222076, they are reduced even more noticeably by 2%, 0.5% and 4.7%. We also note an improvement of 10% for the age of HD 222076 when the Gaia parallax is included as a constraint compared to the case when only the large separation is included as constraint.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
