Search results for " verification"
showing 10 items of 91 documents
Identification and Handling of Critical Irradiance Forecast Errors Using a Random Forest Scheme – A Case Study for Southern Brazil
2015
Abstract Large forecast errors of solar power prediction cause challenges for the management of electric grids. Here, the classification technique Random Forests is applied to analyze the possible linkage of hourly or daily forecast errors to the actual situation given by a set of meteorological variables. This form a prediction of the forecast error and is thus usable to update the forecast. The performance of this scheme is assessed for the example of irradiance forecasts in Brazil. While limited to none improvements are obtained for next-hour forecasts, significant improvements are obtained for the next-day forecasts.
Fingerprint image enhancement using directional morphological filter
2005
Fingerprint images quality enhancement is a topic phase to ensure good performance in an automatic fingerprint identification system (AFIS) based on minutiae matching. In this paper a new fingerprint enhancement algorithm based on morphological filter is introduced. The algorithm is based on three steps: directional decomposition, morphological filter and composition. The performance of the proposed approach has been evaluated on two sets of images: the first one is DB3 database from Fingerprint Verification Competition (FVC) and the second one is self collected using an optical scanner
An Advanced Technique for User Identification Using Partial Fingerprint
2013
User identification is a very interesting and complex task. Invasive biometrics is based on traits uniqueness and immutability over time. In forensic field, fingerprints have always been considered an essential element for personal recognition. The traditional issue is focused on full fingerprint images matching. In this paper an advanced technique for personal recognition based on partial fingerprint is proposed. This system is based on fingerprint local analysis and micro-features, endpoints and bifurcations, extraction. The proposed approach starts from minutiae extraction from a partial fingerprint image and ends with the final matching score between fingerprint pairs. The computation o…
Safety Assurance of a High Voltage Controller for an Industrial Robotic System
2020
Abstract Due to the risk of discharge sparks and ignition, there are strict rules concerning the safety of high voltage electrostatic systems used in industrial painting robots. In order to assure that the system fulfils its safety requirements, formal verification is an important tool to supplement traditional testing and quality assurance procedures. The work in this paper presents formal verification of the most important safety functions of a high voltage controller. The controller has been modelled as a finite state machine, which was formally verified using two different model checking software tools; Simulink Design Verifier and RoboTool. Five safety critical properties were specifie…
Building a new CTL model checker using Web services
2013
This Computation Tree Logic (CTL) is widely used to capture compositions of reactive systems. Model checking is particularly well-suited for the automated verification of finite-state systems, both for software and for hardware. A CTL model checker tool allows designers to automatically verify that systems satisfy specifications expressed in the language of CTL logic. In this paper we present a new CTL model checker implemented in client-server paradigm. CTL Designer, the client tool, allows an interactive construction of the CTL models as state-transition graphs. Java and C# APIs are provided for programmatic construction of large models. The server part of our tool embeds the core of the …
Domain specific language for securities settlement systems
2012
Actual problems during design, implementation and maintenance of securities settlement systems software are achieving complementarity of several different, connected, asynchronously communicating settlement systems and verification of this complementarity. The aim of this paper is to create domain specific language for modeling of settlement systems and their interactions. Then use models to calculate settlement systems behavior. Specific of settlement systems requires that they perform accordingly to business rules in any situation. This makes use of model checking a very desirable step in development process of settlement systems. Defining a domain specific language and creating editor su…
Survey of Formal Verification Methods for Smart Contracts on Blockchain
2019
Due to the immutable nature of distributed ledger technology such as blockchain, it is of utter importance that a smart contract works as intended before employment outside test network. This is since any bugs or errors will become permanent once published to the live network, and could lead to substantial economic losses; as manifested in the infamous DAO smart contract exploit hack in 2016. In order to avoid this, formal verification methods can be used to ensure that the contract behaves according to given specifications. This paper presents a survey of the state of the art of formal verification of smart contracts. Being a relatively new research area, a standard or best practice for fo…
Verifying a medical protocol with temporal graphs: the case of a nosocomial disease.
2014
Abstract Objective Our contribution focuses on the implementation of a formal verification approach for medical protocols with graphical temporal reasoning paths to facilitate the understanding of verification steps. Materials and methods Formal medical guideline specifications and background knowledge are represented through conceptual graphs, and reasoning is based on graph homomorphism. These materials explain the underlying principles or rationale that guide the functioning of verifications. Results An illustration of this proposal is made using a medical protocol defining guidelines for the monitoring and prevention of nosocomial infections. Such infections, which are acquired in the h…
Formal Modeling and Discrete-Time Analysis of BPEL Web Services
2008
International audience; Web services are increasingly used for building enterprise information systems according to the Service Oriented Architecture (SOA) paradigm. We propose in this paper a tool-equipped methodology allowing the formal modeling and analysis of Web services described in the BPEL language. The discrete-time transition systems modeling the behavior of BPEL descriptions are obtained by an exhaustive simulation based on a formalization of BPEL semantics using the Algebra of Timed Processes (ATP). These models are then analyzed by model checking value-based temporal logic properties using the CADP toolbox. The approach is illustrated with the design of a Web service for GPS na…
Integrated Tool for Assisted Predictive Analytics
2021
Organizations use predictive analysis in CRM (customer relationship management) applications for marketing campaigns, sales, and customer services, in manufacturing to predict the location and rate of machine failures, in financial services to forecast financial market trends, predict the impact of new policies, laws and regulations on businesses and markets, etc. Predictive analytics is a business process which consists of collecting the data, developing accurate predictive model and making the analytics available to the business users through a data visualization application. The reliability of a business process can be increased by modeling the process and formally verifying its correctn…