scholarly journals A system for deduction-based formal verification of workflow-oriented software models

2014 ◽  
Vol 24 (4) ◽  
pp. 941-956 ◽  
Author(s):  
Radosław Klimek
Keyword(s):  
Formal Verification ◽  
Temporal Logic ◽  
Business Processes ◽  
Deductive Reasoning ◽  
Main Idea ◽  
Automatic Generation ◽  
Generation Process ◽  
Software Models ◽  
Logical Specifications ◽  
Inexperienced User

Abstract The work concerns formal verification of workflow-oriented software models using the deductive approach. The formal correctness of a model’s behaviour is considered. Manually building logical specifications, which are regarded as a set of temporal logic formulas, seems to be a significant obstacle for an inexperienced user when applying the deductive approach. A system, along with its architecture, for deduction-based verification of workflow-oriented models is proposed. The process inference is based on the semantic tableaux method, which has some advantages when compared with traditional deduction strategies. The algorithm for automatic generation of logical specifications is proposed. The generation procedure is based on predefined workflow patterns for BPMN, which is a standard and dominant notation for the modeling of business processes. The main idea behind the approach is to consider patterns, defined in terms of temporal logic, as a kind of (logical) primitives which enable the transformation of models to temporal logic formulas constituting a logical specification. Automation of the generation process is crucial for bridging the gap between the intuitiveness of deductive reasoning and the difficulty of its practical application when logical specifications are built manually. This approach has gone some way towards supporting, hopefully enhancing, our understanding of deduction-based formal verification of workflow-oriented models.

Ein Ansatz zur formalen Verifikation von Schaltungsbeschreibungen in SystemC (An Approach for Formal Verification of Circuits in SystemC)

2003 ◽  
Vol 45 (4) ◽  
Author(s):  
Daniel Große ◽  
Rolf Drechsler
Keyword(s):  
Formal Verification ◽  
Temporal Logic ◽  
Linear Time ◽  
Linear Time Temporal Logic

ZusammenfassungDer vorgestellte Ansatz ermöglicht es, für SystemC-Schaltkreisbeschreibungen, die über einer gegebenen Gatterbibliothek definiert sind, Eigenschaften zu beweisen (engl. property checking). Als Spezifikationssprache wird LTL (linear time temporal logic) verwendet. Für den Beweis einer LTL-Eigenschaft kann die Erfüllbarkeit einer Booleschen Funktion betrachtet werden, die aus der Eigenschaft und der Schaltkreisbeschreibung mittels symbolischer Methoden konstruiert wird. Im Gegensatz zu simulationsbasierten Ansätzen kann dabei Vollständigkeit gewährleistet werden. Anhand einer Fallstudie eines skalierbaren Arbiters wird die Effizienz des Beweisverfahrens untersucht.

Modeling and Specification of Collaborative Business Processes with a MDA Approach and a UML Profile

2010 ◽  
pp. 238-268
Author(s):  
Pablo David Villarreal ◽  
Enrique Salomone ◽  
Omar Chiotti
Keyword(s):  
Business Processes ◽  
Conceptual Modeling ◽  
Automatic Generation ◽  
Uml Profile ◽  
Analysis And Design ◽  
Model Driven ◽  
Collaborative Processes ◽  
Interaction Protocols ◽  
Business To Business

This chapter describes the application of MDA (model driven architecture) and UML for the modeling and specification of collaborative business processes, with the purpose of enabling enterprises to establish business-to-business collaborations. The proposed MDA approach provides the components and techniques required for the development of collaborative processes from their conceptual modeling to the specifications of these processes and the partners’ interfaces in a B2B standard. As part of this MDA approach, a UML profile is provided that extends the semantics of UML2 to support the analysis and design of collaborative processes. This UML profile is based on the use of interaction protocols to model collaborative processes. The application of this UML profile in a case study is presented. Also, an overview is provided about the automatic generation of B2B specifications from conceptual models of collaborative processes. In particular, the generation of B2B specifications based on ebXML is described.

Model Checking for SpaceWire Error Detection Module

2012 ◽  
Vol 241-244 ◽  
pp. 3020-3025
Author(s):  
Ling Ling Dong ◽  
Yong Guan ◽  
Xiao Juan Li ◽  
Zhi Ping Shi ◽  
Jie Zhang ◽  
...  
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Temporal Logic ◽  
Error Detection ◽  
System Model ◽  
Linear Search ◽  
Kripke Structure ◽  
Mathematical Methods ◽  
Safety Critical ◽  
Correctness Of Programs

Considerable attention has been devoted to prove the correctness of programs. Formal verification overcomes the incompleteness by applying mathematical methods to verify a design. SpaceWire is a well known communication standard. For safety-critical applications an approach is needed to validate the completeness of SpareWire design. This paper addresses formal verification of SpareWire error detection module. The system model was constructed by Kripke structure, and the properties were presented by linear temporal logic (LTL). Compared the verification of LTL with CTL (branch temporal logic), LTL properties could improve the verification efficiency due to its linear search. The error priority was checked using simulation guided by model checking. After some properties were modified, all possible behaviors of the module satisfied the specification. This method realizes complete validation of the error detection module.

CAD Information Handling for Obtaining Dependable Manufacturing Systems

2015 ◽  
Author(s):  
E. Miron ◽  
J. P. Mendonca ◽  
J. Machado ◽  
D. Olaru ◽  
G. Prisacaru
Keyword(s):  
Formal Verification ◽  
Manufacturing Systems ◽  
Specific Problem ◽  
Main Idea ◽  
Software As A Service ◽  
Model Checker ◽  
Mechatronic Systems ◽  
Analysis Techniques ◽  
Successful Design ◽  
High Level

The design of mechatronic systems is a multidisciplinary task that involves skills from mechanic, electronic and informatics areas. Recently, the expertise from such different fields is able to communicate and exchange the necessary contribution to successful design solutions, through a myriad of internet tools available. The introduction of internet of services on the design of mechatronic systems, mainly when teams, with different skills, operate in different geographic places, has contributed to flawlessly integrate better and interoperable final solutions. The design of mechatronic systems without errors — that operate without failures — is an important contribution to such goal. Safe behavior of mechatronic systems is crucial, mainly, in what concerns human safety. The correct behavior of those systems can be improved by the development of safe software for their controllers using some analysis techniques. Among them, Formal Verification (FV) is able to guarantee the best results. One of the main gaps using this technique is the difficulty of obtaining adequate plant models, in a systematic way, because this task is, usually, related with high level of expertise of designers and, in industry, this fact causes some difficulties for using those methods and tools. The work presented in this paper is a part of a larger project developed in the context of Software as a Service (SaaS) platform. It is intended to develop a systematized approach in order to obtain meaningful plant models out of existing CAD data, from Autodesk Inventor (or CATIA), and translate those models to formatted files according to input data of the UPPAAL model-checker (because it allows dealing with time variable). The main idea is to obtain, systematically, plant models for Formal Verification purposes, considering that nowadays companies with different CAD systems are using increasingly often STEP-File format. A solution for this specific problem is explored and presented in this paper.

Semantic Business Process Integration in Cloud Manufacturing Paradigm

2012 ◽  
Vol 235 ◽  
pp. 379-383 ◽  
Author(s):  
Yun Bo Zeng
Keyword(s):  
Business Process ◽  
Manufacturing Industry ◽  
Business Processes ◽  
Process Integration ◽  
Main Idea ◽  
Cloud Manufacturing ◽  
Distributed Resources ◽  
Manufacturing Resources ◽  
Business Process Execution ◽  
Detailed Presentation

Global competition in the manufacturing industry forces to build a cross-organizational business process cooperative environment, in which manufacturers can share and utilize distributed resources and competencies for rapidly and cost-effectively developing products. But the varying manufacturing resources are heterogeneity which limits the business process execution in an automated way. This paper presents an approach for cross-organizational business processes integration in the cloud manufacturing paradigm. The main idea is to encapsulate an organization’s resources and competencies within appropriate interfaces and advertise it as semantic web services, called manufacturing service. An executable business process is achieved by manufacturing services composition. We give a detailed presentation of the cloud manufacturing service model. Semantically description of service not only contains resources’ capability, but also is considered as mediators to bridge the gap between the modeled processes and their implementation. The main integration process is introduced based our approach.

Sign in / Sign up

Export Citation Format

Share Document