Статті в журналах з теми "Model and Program Verification"
Щоб переглянути інші типи публікацій з цієї теми, перейдіть за посиланням: Model and Program Verification.
Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями
Ознайомтеся з топ-50 статей у журналах для дослідження на тему "Model and Program Verification".
Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.
Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.
Переглядайте статті в журналах для різних дисциплін та оформлюйте правильно вашу бібліографію.
1
Yim, Joon-Seo, Chang-Jae Park, In-Cheol Park, and Chong-Min Kyung. "Design Verification of Complex Microprocessors." Journal of Circuits, Systems and Computers 07, no. 04 (August 1997): 301–18. http://dx.doi.org/10.1142/s021812669700022x.
Анотація:
As the complexity of microprocessors increases, functional verification becomes more difficult and emerges as the bottleneck of the design cycle. In this paper, we suggest a functional verification methodology, especially for compatible microprocessor designs. To guarantee perfect compatibility with previous microprocessors, we developed three C models in different abstraction levels, i.e. Polaris, MCV and StreC. An instruction behavioral level C model (Polaris) is verified using the slowed-down PC. In the implemetation of micro-architecture, a micro-operational level model (MCV) and RTL model (StreC) are co-simulated with consistency checking between these two models. The simulation speed of C models makes it possible to test the "real-world" application programs on the RTL design with a software board model (VPC). To increase the confidence level of verifications, Profiler reports the verification coverage of the test program, which is fed-back to the automatic test program generator (Pandora). The Restartability feature also helps to significantly reduce the total simulation time. Using the proposed verification methodology, we designed and verified the HK486, an Intel 80486 pin-compatible microprocessor successfully.
2
He, Pei, Achun Hu, Dongqing Xie, and Zhiping Fan. "Component-Based Verification Model of Sequential Programs." Journal of Software 10, no. 11 (November 2015): 1319–26. http://dx.doi.org/10.17706//jsw.10.11.1319-132.
3
Zelkowitz, M. V. "A functional correctness model of program verification." Computer 23, no. 11 (November 1990): 30–39. http://dx.doi.org/10.1109/2.60878.
4
Gregorics, Tibor, and Zsolt Borsi. "A unified approach of program verification." Acta Universitatis Sapientiae, Informatica 9, no. 1 (July 26, 2017): 65–82. http://dx.doi.org/10.1515/ausi-2017-0005.
Анотація:
Abstract The subject of this paper is a program verification method that takes into account abortion caused by partial functions in program statements. In particular, boolean expressions of various statements will be investigated that are not well-defined. For example, a loop aborts if its execution begins in a state for which the loop condition is undefined. This work considers the program constructs of nondeterministic sequential programs and also deals with the synchronization statement of parallel programs introduced by Owicki and Gries [7]. The syntax of program constructs will be reviewed and their semantics will be formally defined in such a way that they suit the relational model of programming developed at Eőtvős Loránd University [3, 4]. This relational model defines the program as a set of its possible executions and also provides definition for other important programming notions like problem and solution. The proof rules of total correctness [2, 5, 8, 9, 7] will be extended by treating abortion caused by partial functions. The use of these rules will be demonstrated by means of a verification case study.
5
DE ANGELIS, EMANUELE, FABIO FIORAVANTI, ALBERTO PETTOROSSI, and MAURIZIO PROIETTI. "Predicate Pairing for program verification." Theory and Practice of Logic Programming 18, no. 2 (December 4, 2017): 126–66. http://dx.doi.org/10.1017/s1471068417000497.
Анотація:
AbstractIt is well-known that the verification of partial correctness properties of imperative programs can be reduced to the satisfiability problem for constrained Horn clauses (CHCs). However, state-of-the-art solvers for constrained Horn clauses (or CHC solvers) based onpredicate abstractionare sometimes unable to verify satisfiability because they look for models that are definable in a given class 𝓐 of constraints, called 𝓐-definable models. We introduce a transformation technique, calledPredicate Pairing, which is able, in many interesting cases, to transform a set of clauses into an equisatisfiable set whose satisfiability can be proved by finding an 𝓐-definable model, and hence can be effectively verified by a state-of-the-art CHC solver. In particular, we prove that, under very general conditions on 𝓐, the unfold/fold transformation rules preserve the existence of an 𝓐-definable model, that is, if the original clauses have an 𝓐-definable model, then the transformed clauses have an 𝓐-definable model. The converse does not hold in general, and we provide suitable conditions under which the transformed clauses have an 𝓐-definable modelif and only ifthe original ones have an 𝓐-definable model. Then, we present a strategy, called Predicate Pairing, which guides the application of the transformation rules with the objective of deriving a set of clauses whose satisfiability problem can be solved by looking for 𝓐-definable models. The Predicate Pairing (PP) strategy introduces a new predicate defined by the conjunction of two predicates occurring in the original set of clauses, together with a conjunction of constraints. We will show through some examples that an 𝓐-definable model may exist for the new predicate even if it does not exist for its defining atomic conjuncts. We will also present some case studies showing that Predicate Pairing plays a crucial role in the verification ofrelational properties of programs, that is, properties relating two programs (such as program equivalence) or two executions of the same program (such as non-interference). Finally, we perform an experimental evaluation of the proposed techniques to assess the effectiveness of Predicate Pairing in increasing the power of CHC solving.
6
Luo, Min. "Model Extraction and Reliability Verification on SOCKET Program." Advanced Materials Research 616-618 (December 2012): 2055–59. http://dx.doi.org/10.4028/www.scientific.net/amr.616-618.2055.
Анотація:
Formal method is a means to verify the reliability and safety of concurrent systems. Formal verification of model which automatically extracted from concurrent system built from high level language is a hot research topic in the field of model checking technology. With the focus on potential run time problems (deadlocks, memory leaks, the boundary data loss and other run-time errors) result from abnormal socket function call sequence, we analyze the sequence structure of the socket program and construct the Promela model of socket functions through the description of message data structures and channels, as well as define mapping rules of socket function to Promela. The socket function call sequence extraction algorithm and target Promela model generation algorithm are proposed by using linear temporal logic (LTL) to describe the property the socket function call sequence. A socket communication program analysis system has been constructed. The experiment result shows that the system can detect the potential run time problems of socket program effectively.
7
Yamane, Satoshi. "Deductive Verification Method of Real-Time Safety Properties for Embedded Assembly Programs." Electronics 8, no. 10 (October 14, 2019): 1163. http://dx.doi.org/10.3390/electronics8101163.
Анотація:
It is important to verify both the correctness and real-time properties of embedded systems. However, as practical computer programs are represented by infinite state transition systems, specifying and verifying a computer program is difficult. Real-time properties are also important for embedded programs, but verifying the real-time properties of an embedded program is difficult. In this paper, we focus on verifying an embedded assembly program, in order to verify the real-time safety properties. We propose a deductive verification method to verify real-time safety properties, based on discrete time, as follows: (1) First, we construct a timed computational model including the execution time from the assembly program. We can specify an infinite state transition system including the execution time of the timed computational model. (2) Next, we verify whether a timed computational model satisfies RTLTL (Real-Time Linear Temporal Logic) formulas by deductive verification. We can specify real-time properties by RTLTL. By our proposed methods, we are able to achieve verification of the real-time safety properties of an embedded program.
8
Neyzov, Maxim V., and Egor V. Kuzmin. "LTL-specification for development and verification of control programs." Modeling and Analysis of Information Systems 30, no. 4 (December 11, 2023): 308–39. http://dx.doi.org/10.18255/1818-1015-2023-4-308-339.
Анотація:
This work continues the series of articles on development and verification of control programs based on the LTL-specification. The essence of the approach is to describe the behavior of programs using formulas of linear temporal logic LTL of a special form. The developed LTL-specification can be directly verified by using a model checking tool. Next, according to the LTL-specification, the program code in the imperative programming language is unambiguously built. The translation of the specification into the program is carried out using a template. The novelty of the work consists in the proposal of two LTL-specifications of a new form — declarative and imperative, as well as in a more strict formal justification for this approach to program development and verification. A transition has been made to a more modern verification tool for finite and infinite systems — nuXmv. It is proposed to describe the behavior of control programs in a declarative style. For this purpose, a declarative LTL-specification is intended, which defines a labelled transition system as a formal model of program behavior. This method of describing behavior is quite expressive — the theorem on the Turing completeness of the declarative LTL-specification is proved. Next, to construct program code in an imperative language, the declarative LTL-specification is converted into an equivalent imperative LTL-specification. An equivalence theorem is proved, which guarantees that both specifications specify the same behavior. The imperative LTL-specification is translated into imperative program code according to the presented template. The declarative LTL-specification, which is subject to verification, and the control program built on it are guaranteed to specify the same behavior in the form of a corresponding transition system. Thus, during verification, a model is used that is adequate to the real behavior of the control program.
9
ZUO, Zhengkang, Ying HU, Qing HUANG, Yuan WANG, and Changjing WANG. "Automatic Algorithm Programming Model Based on the Improved Morgan's Refinement Calculus." Wuhan University Journal of Natural Sciences 27, no. 5 (October 2022): 405–14. http://dx.doi.org/10.1051/wujns/2022275405.
Анотація:
The automatic algorithm programming model can increase the dependability and efficiency of algorithm program development, including specification generation, program refinement, and formal verification. However, the existing model has two flaws: incompleteness of program refinement and inadequate automation of formal verification. This paper proposes an automatic algorithm programming model based on the improved Morgan's refinement calculus. It extends the Morgan's refinement calculus rules and designs the C++ generation system for realizing the complete process of refinement. Meanwhile, the automation tools VCG (Verification Condition Generator) and Isabelle are used to improve the automation of formal verification. An example of a stock's maximum income demonstrates the effectiveness of the proposed model. Furthermore, the proposed model has some relevance for automatic software generation.
10
Kuzmin, E. V., and V. A. Sokolov. "On Construction and Verification of PLC-Programs." Modeling and Analysis of Information Systems 19, no. 4 (February 28, 2015): 25–36. http://dx.doi.org/10.18255/1818-1015-2012-4-25-36.
Анотація:
We review some methods and approaches to programming discrete problems for Programmable Logic Controllers on the example of constructing PLC-programs for controling a code lock. For these approaches we evaluate the usability of the model checking method for the analysis of program correctness with respect to the automatic verification tool Cadence SMV. Some possible PLC-program vulnerabilities arising at a number approaches to programming of PLC are revealed.
11
Vega Vice, Jorge, and Valery Mikhailov. "On Methods in the Verification and Elaboration of Development Programs for Agricultural Territories." Modeling and Analysis of Information Systems 25, no. 5 (October 28, 2018): 481–90. http://dx.doi.org/10.18255/1818-1015-2018-5-481-490.
Анотація:
Nowadays, the methods of program-targeted management for the development of various socio-economic systems of complex structure, such as agricultural areas, have become universal. Therefore, the current tasks at hand are the verification of already created development programs and the development of "proper" programs for the development of such systems, by analogy with the verification and development of proper computer programs through developed disciplines in theoretical programming. In this paper, in order to solve the problem of verification of development programs for agricultural territories, a structural scheme of the program is first constructed, through which the axiomatic theory is created, using Hoare’s algorithmic logic system. The main problem in the construction of the axiomatic theory is the development of the axioms of the theory reflecting the preconditions and effects of the implementation of meaningful actions indicated in the text of the development program. The verification of the development program corresponds to the probability of some Hoare triplet, according to the initial and target conditions of the program. For the task of elaboration of the right development programs, the mechanism for constructing a domain model using the PDDL family description languages is described. The description of a specific model is purely declarative in nature and consists of descriptions of predicates and actions of the chosen subject area. In this paper, it is shown how on the described model with the help of intelligent planners, including temporal planners such as OPTIC, solutions to the targets of development programs can be automatically built. Based on expert knowledge and activity standards, a model of an agricultural territory is constructed, a brief description of which is given in the work. The conducted experiments showed the effectiveness of the proposed approach for the development of proper development programs.
12
Darvas, Dániel, István Majzik, and Enrique Blanco Viñuela. "PLC Program Translation for Verification Purposes." Periodica Polytechnica Electrical Engineering and Computer Science 61, no. 2 (May 23, 2017): 151. http://dx.doi.org/10.3311/ppee.9743.
Анотація:
Programmable logic controllers are typically programmed in one of the five languages defined in the IEC 61131 standard. While the ability to choose the appropriate language for each program unit may be an advantage for the developers, it poses a serious challenge to verification methods. In this paper we analyse and compare these languages to show that the ST programming language can efficiently and conveniently represent all PLC languages for formal verification purposes. Furthermore, we provide a translation method from IL to ST programming languages (for the Siemens implementation), together with a sketch of proof for its correctness. This allows the usage of the ST-based PLCverif model checking method for safety PLC programs.
13
Petrov, Oleg Maximovich. "Finding More Bugs with Software Model Checking using Delta Debugging." Proceedings of the Institute for System Programming of the RAS 35, no. 3 (2023): 151–62. http://dx.doi.org/10.15514/ispras-2023-35(3)-11.
Анотація:
Many verification tasks in model checking (one of the formal software verification approaches) can’t be solved within bounded time requirements due to combinatorial state space explosion. In order to find a bug in the verified program in a given time, a simplified version of it can be analyzed. This paper presents DD** algorithms (based on the Delta Debugging approach) to iterate over simplified versions of the given program. These algorithms were implemented in software-verification tool CPAchecker. Our experiments showed that this technique might be used to find new bugs in real software.
14
KUDLAI, Vladyslav, Nataliia BONDARENKO, and Viktor BONDARENKO. "CONSTRUCTION AND VERIFICATION OF A DIGITAL EQUALIZER MODEL." Herald of Khmelnytskyi National University. Technical sciences 313, no. 5 (October 27, 2022): 178–84. http://dx.doi.org/10.31891/2307-5732-2022-313-5-178-184.
Анотація:
An approach to the development of an equalizer by building its mathematical model based on a microcontroller is proposed. All operations, including signal processing and equalizer kernel calculation, are performed by a single microcontroller. Thanks to the created mathematical model of the equalizer, the calculation of the kernel is reduced to multiple uses of relatively simple operations, which saves time and memory of the program. The equalizer provides satisfactory processing quality at a small filter order which is selected as a digital filter with final impulse response (FIR) because of its linear phase-frequency response, a guarantee of stability at the complex amplitude-frequency response, and also its associativity and linearity allowing it easily reproduce a complex amplitude-frequency response. Schematic implementation is based on parallel bandpass filters and a low-pass filter followed by adding filtered and amplified signals. It is the distributive property of the FIR filter that makes it possible to obtain a new kernel that includes all the amplified ranges by the sum of the corresponding kernel elements, instead of adding amplified ranges. The associativity and linearity of the FIR filter gives the opportunity to easily implement different types of filters on the basis of a low-pass filter, for the calculation of which the cardinal sine function is used together with the window function, which in combination gives qualitative frequency characteristics. The low-pass filter kernel and equalizer model are verified in the GNU Octave environment, which is an open-source analogue of Matlab. The model is checked by setting the frequency response of the test equalizer, and for individual filters the allowable width of the transition band and the maximum value of pulsation in the suppression band are set. The low-pass filter kernel is created with an arbitrary cutoff frequency, and the filter consists of 129 elements, which were multiplied by the Kaiser window with a value of parameter equal to 4.5. As a result of verification of the mathematical model in the GNU Octave environment, the width of the transition band and the maximum value of pulsation in the suppression band meet the specified conditions. The simulated equalizer kernel fully corresponds to the specified frequency response. Verification of the mathematical model confirmed its efficiency and compliance of the obtained characteristics of the equalizer with the specified requirements.
15
Neyzov, Maxim V., and Egor V. Kuzmin. "Verification of declarative LTL-specification of control programs behavior." Modeling and Analysis of Information Systems 31, no. 2 (June 13, 2024): 120–41. http://dx.doi.org/10.18255/1818-1015-2024-2-120-141.
Анотація:
The article continues the series of works on development and verification of control programs based on LTL-specifications of a special type. Previously, it was proposed a declarative LTL-specification, which allows describing the behavior of control programs and building program code based on it in the imperative ST-language for programmable logic controllers. The LTL-specification can be directly verified for compliance with specified temporal properties by the model checking method using the nuXmv symbolic verification tool. In general, it is not required translating LTL-formulas of the specification into another formalism — an SMV-specification (code in the input language of the nuXmv tool). The purpose of this work is to explore alternative ways of representing a program behavior model corresponding to the declarative LTL-specification during its verification within the nuXmv tool. In the article, we transform the declarative LTL-specification into various SMV-specifications with accompanying changes of formulation of the verification problem, what leads to a significant reduction in time costs when checking temporal properties by using the nuXmv tool. The acceleration of verification is due to the reduction of the state space of a model being verified. The SMV-specifications obtained as a result of the proposed transformations specify identical or bisimulationally equivalent transition systems. It is ensuring the same verification results when replacing one SMV-specification with another.
16
Garanina, Natalia Olegovna, and Sergei Petrovich Gorlatch. "Autotuning Parallel Programs by Model Checking." Modeling and Analysis of Information Systems 28, no. 4 (December 18, 2021): 338–55. http://dx.doi.org/10.18255/1818-1015-2021-4-338-355.
Анотація:
The paper presents a new approach to autotuning data-parallel programs. Autotuning is a search for optimal program settings which maximize its performance. The novelty of the approach lies in the use of the model checking method to find the optimal tuning parameters by the method of counterexamples. In our work, we abstract from specific programs and specific processors by defining their representative abstract patterns. Our method of counterexamples implements the following four steps. At the first step, an execution model of an abstract program on an abstract processor is described in the language of a model checking tool. At the second step, in the language of the model checking tool, we formulate the optimality property that depends on the constructed model. At the third step, we find the optimal values of the tuning parameters by using a counterexample constructed during the verification of the optimality property. In the fourth step, we extract the information about the tuning parameters from the counter-example for the optimal parameters. We apply this approach to autotuning parallel programs written in OpenCL, a popular modern language that extends the C language for programming both standard multi-core processors (CPUs) and massively parallel graphics processing units (GPUs). As a verification tool, we use the SPIN verifier and its model representation language Promela, whose formal semantics is good for modelling the execution of parallel programs on processors with different architectures.
17
Shelekhov, V. I., and E. G. Tumurov. "Automata-based Software Engineering for Control System Design and Verification." Programmnaya Ingeneria 15, no. 2 (February 19, 2024): 73–86. http://dx.doi.org/10.17587/prin.15.73-86.
Анотація:
The automata composition is defined as the basic language construct of automata programming. Incorporating automata composition into an arbitrary programming language allows the development of automata programs in that language. Methods for specification and verification of reactive systems are defined in detail. All kinds of correctness formulas for a reactive system with respect to its specification are defined. In addition, correctness formulas for verification using the full invariant of the reactive system are developed. The Event-B manual begins with a brilliant illustration of the basic Event-B methods using the example of a car traffic control problem on a narrow bridge. However, the latter refinement in this illustration generates a complex cumbersome program. A simpler and shorter solution to this problem was presented in our work [7] using automata programming approach. Our solution was not easy because 4 non-trivial bugs were found by verification in Event-B. This paper describes our third attempt to construct a short simple automata program to solve this problem. Verification of the automata program in Event-B and Why3 systems was carried out. No errors were found. For verification, a reactive system model is built on Why3, which is simpler and more universal than the why3-do model.
18
Metzler, Patrick, Neeraj Suri, and Georg Weissenbacher. "Extracting safe thread schedules from incomplete model checking results." International Journal on Software Tools for Technology Transfer 22, no. 5 (June 26, 2020): 565–81. http://dx.doi.org/10.1007/s10009-020-00575-y.
Анотація:
Abstract Model checkers frequently fail to completely verify a concurrent program, even if partial-order reduction is applied. The verification engineer is left in doubt whether the program is safe and the effort toward verifying the program is wasted. We present a technique that uses the results of such incomplete verification attempts to construct a (fair) scheduler that allows the safe execution of the partially verified concurrent program. This scheduler restricts the execution to schedules that have been proven safe (and prevents executions that were found to be erroneous). We evaluate the performance of our technique and show how it can be improved using partial-order reduction. While constraining the scheduler results in a considerable performance penalty in general, we show that in some cases our approach—somewhat surprisingly—even leads to faster executions.
19
FIORAVANTI, FABIO, ALBERTO PETTOROSSI, MAURIZIO PROIETTI, and VALERIO SENNI. "Generalization strategies for the verification of infinite state systems." Theory and Practice of Logic Programming 13, no. 2 (January 25, 2012): 175–99. http://dx.doi.org/10.1017/s1471068411000627.
Анотація:
AbstractWe present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic programs (CLP) and works in two phases: (1) in the first phase, a CLP specification of an infinite state system is specialized with respect to the initial state of the system and the temporal property to be verified, and (2) in the second phase, the specialized program is evaluated by using a bottom-up strategy. The effectiveness of the method strongly depends on the generalization strategy which is applied during the program specialization phase. We consider several generalization strategies obtained by combining techniques already known in the field of program analysis and program transformation, and we also introduce some new strategies. Then, through many verification experiments, we evaluate the effectiveness of the generalization strategies we have considered. Finally, we compare the implementation of our specialization-based verification method to other constraint-based model checking tools. The experimental results show that our method is competitive with the methods used by those other tools.
20
Hidayati, Wildani. "EVALUATION OF MEMORIES LEARNING PROGRAM AL-QUR'AN AS A LOCAL CURRICULUM AT MTs.N 7 MODUR JAKARTA TIMUR (Evaluative Research Using CSE-UCLA Models)." JISAE: Journal of Indonesian Student Assessment and Evaluation 4, no. 2 (September 4, 2019): 1–12. http://dx.doi.org/10.21009/jisae.v4i2.8289.
Анотація:
Abstract
This study aims to find out how effective the implementation of Qur'anic learning in MTs.N 7 East Jakarta models. This study is classified as evaluative research using the CSE-UCLA model consisting of assessment, program planning, implementation programs, programs improvement and program certification. The subject of this study consisted of: school principal, mentor, student and student guardian. Data collection methods are carried out with questionnaires, observation, interviews, and documentation. Data analysis techniques in this study are the Miles and Huburmen models. The activity in data analysis is data reduction , data display (data presentation), and conclusion drawing / verification (drawing conclusions / verification). The research findings show that the Al-Qur'an learning program has been running effectively even though there are obstacles that need to be corrected
21
Hidayati, Wildani. "EVALUATION OF MEMORIES LEARNING PROGRAM AL-QUR'AN AS A LOCAL CURRICULUM AT MTs.N 7 MODUR JAKARTA TIMUR (Evaluative Research Using CSE-UCLA Models)." JISAE: JOURNAL OF INDONESIAN STUDENT ASSESMENT AND EVALUATION 4, no. 2 (September 4, 2019): 1–12. http://dx.doi.org/10.21009/jisae.042.01.
Анотація:
Abstract
This study aims to find out how effective the implementation of Qur'anic learning in MTs.N 7 East Jakarta models. This study is classified as evaluative research using the CSE-UCLA model consisting of assessment, program planning, implementation programs, programs improvement and program certification. The subject of this study consisted of: school principal, mentor, student and student guardian. Data collection methods are carried out with questionnaires, observation, interviews, and documentation. Data analysis techniques in this study are the Miles and Huburmen models. The activity in data analysis is data reduction , data display (data presentation), and conclusion drawing / verification (drawing conclusions / verification). The research findings show that the Al-Qur'an learning program has been running effectively even though there are obstacles that need to be corrected
22
Sun, Zhihang, Hongyu Fan, and Fei He. "Consistency-preserving propagation for SMT solving of concurrent program verification." Proceedings of the ACM on Programming Languages 6, OOPSLA2 (October 31, 2022): 929–56. http://dx.doi.org/10.1145/3563321.
Анотація:
The happens-before orders have been widely adopted to model thread interleaving behaviors of concurrent programs. A dedicated ordering theory solver, usually composed of theory propagation, consistency checking, and conflict clause generation, plays a central role in concurrent program verification. We propose a novel preventive reasoning approach that automatically preserves the ordering consistency and makes consistency checking and conflict clause generation omissible. We implement our approach in a prototype tool and conduct experiments on credible benchmarks; results reveal a significant improvement over existing state-of-the-art concurrent program verifiers.
23
Sherman, Elena, Yannic Noller, Cyrille Artho, Franck van Breugel, Anto Nanah Ji, John Kellerman, Parssa Khazra, et al. "The Java Pathfinder Workshop 2022." ACM SIGSOFT Software Engineering Notes 48, no. 1 (January 10, 2023): 19–21. http://dx.doi.org/10.1145/3573074.3573080.
Анотація:
Java Pathfinder (JPF) was originally developed as an explicit state software model checker and subsequently evolved into an extensible Java bytecode analysis framework that has been successfully used to implement techniques such as symbolic and concolic execution, compositional verification, parallel execution, incremental program analysis, and many more. Apart from its original domain of concurrent Java programs, JPF now supports the verification of new domains such as UMLs, numeric programs, graphical user interfaces, and Android applications.
24
Xiong, Jiawen, Gang Zhu, Yanhong Huang, and Jianqi Shi. "A User-Friendly Verification Approach for IEC 61131-3 PLC Programs." Electronics 9, no. 4 (March 28, 2020): 572. http://dx.doi.org/10.3390/electronics9040572.
Анотація:
Programmable logic controllers (PLCs) are special embedded computers that are widely used in industrial control systems. To ensure the safety of industrial control systems, it is necessary to verify the correctness of PLCs. Formal verification is considered to be an effective method to verify whether a PLC program conforms to its specifications, but the expertise requirements and the complexity make it hard to be mastered and widely applied. In this paper, we present a specification-mining-based verification approach for IEC 61131-3 PLC programs. It only requires users to review specifications mined from the program behaviors instead of model checking for specified specifications, which can greatly improve the efficiency of safety verification and is much easier for control system engineers to use. Moreover, we implement a proof-of-concept tool named PLCInspector that supports directly mining LTL specifications and data invariants from PLC programs. Two examples and one real-life case study are presented to illustrate its practicability and efficiency. In addition, a comparison with the existing verification approaches for PLC programs is discussed.
25
Fu, Yujian, Jeffery Kulick, Lok K. Yan, and Steven Drager. "Formal Modeling and Verification of Security Property in Handel C Program." International Journal of Secure Software Engineering 3, no. 3 (July 2012): 50–65. http://dx.doi.org/10.4018/jsse.2012070103.
Анотація:
Multi-million gate system-on-chip (SoC) designs easily fit into today’s Field Programmable Gate Arrays (FPGAs). As FPGAs become more common in safety-critical and mission-critical systems, researchers and designers require information flow guarantees for the FPGAs. Tools for designing a secure system of chips (SOCs) using FPGAs and new techniques to manage and analyze the security properties precisely are desirable. In this work we propose a formal approach to model, analyze and verify a typical set of security properties – noninterference – of Handel C programs using Petri Nets and model checking. This paper presents a method to model Handel C programs using Predicate Transition Nets, a type of Petri Net, and define security properties on the model, plus a verification approach where security properties are checked. Three steps are used. First, a formal specification on the Handel C description using Petri Nets is extracted. Second, the dynamic noninterference properties with respect to the Handel C program statements are defined on the model. To assist in verification, a translation rule from the Petri Nets specification to the Maude programming language is also defined. Thus, the formal specification can be verified against the system properties using model checking. A case study of the pipeline multiplier is discussed to illustrate the concept and validate the approach.
26
Fan, Kaixuan, and Meng Wang. "DAG-Based Formal Modeling of Spark Applications with MSVL." Information 14, no. 12 (December 12, 2023): 658. http://dx.doi.org/10.3390/info14120658.
Анотація:
Apache Spark is a high-speed computing engine for processing massive data. With its widespread adoption, there is a growing need to analyze its correctness and temporal properties. However, there is scarce research focused on the verification of temporal properties in Spark programs. To address this gap, we employ the code-level runtime verification tool UMC4M based on the Modeling, Simulation, and Verification Language (MSVL). To this end, a Spark program S has to be translated into an MSVL program M, and the negation of the property P specified by a Propositional Projection Temporal Logic (PPTL) formula that needs to be verified is also translated to an MSVL program M1; then, a new MSVL program “M and M1” can be compiled and executed. Whether program S violates the property P is determined by the existence of an acceptable execution of “M and M1”. Thus, the key issue lies in how to formalize model Spark programs using MSVL programs. We previously proposed a solution to this problem—using the MSVL functions to perform Resilient Distributed Datasets (RDD) operations and converting the Spark program into an MSVL program based on the Directed Acyclic Graph (DAG) of the Spark program. However, we only proposed this idea. Building upon this foundation, we implement the conversion from RDD operations to MSVL functions and propose, as well as implement, the rules for translating Spark programs to MSVL programs based on DAG. We confirm the feasibility of this approach and provide a viable method for verifying the temporal properties of Spark programs. Additionally, an automatic translation tool, S2M, is developed. Finally, a case study is presented to demonstrate this conversion process.
27
Mironov, Andrew M. "A Mathematical Model of Parallel Programs and an Approach Based on it to Verification of MPI Programs." Modeling and Analysis of Information Systems 28, no. 4 (December 18, 2021): 394–412. http://dx.doi.org/10.18255/1818-1015-2021-4-394-412.
Анотація:
The paper presents a new mathematical model of parallel programs, on the basis of which it is possible, in particular, to verify parallel programs presented on a certain subset of the parallel programming interface MPI. This model is based on the concepts of a sequential and distributed process. A parallel program is modeled as a distributed process in which sequential processes communicate by asynchronously sending and receiving messages over channels. The main advantage of the described model is the ability to simulate and verify parallel programs that generate an indefinite number of sequential processes. The proposed model is illustrated by the application of verification of the matrix multiplication MPI program.
28
Inverso, Omar, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. "Bounded Verification of Multi-threaded Programs via Lazy Sequentialization." ACM Transactions on Programming Languages and Systems 44, no. 1 (March 31, 2022): 1–50. http://dx.doi.org/10.1145/3478536.
Анотація:
Bounded verification techniques such as bounded model checking (BMC) have successfully been used for many practical program analysis problems, but concurrency still poses a challenge. Here, we describe a new approach to BMC of sequentially consistent imperative programs that use POSIX threads. We first translate the multi-threaded program into a nondeterministic sequential program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. We then reuse existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so it produces tight SAT/SMT formulae, and is thus very effective in practice: Our Lazy-CSeq tool implementing this translation for the C programming language won several gold and silver medals in the concurrency category of the Software Verification Competitions (SV-COMP) 2014–2021 and was able to find errors in programs where all other techniques (including testing) failed. In this article, we give a detailed description of our translation and prove its correctness, sketch its implementation using the CSeq framework, and report on a detailed evaluation and comparison of our approach.
29
Dong, Zhijiang, Yujian Fu, and Yue Fu. "Runtime Verification on Robotics Systems." International Journal of Robotics Applications and Technologies 3, no. 1 (January 2015): 23–40. http://dx.doi.org/10.4018/ijrat.2015010102.
Анотація:
Runtime verification is a technique for generating monitors from formal specification of expected behaviors for the underlying system. It can be applied to automatically evaluate system execution, either on-line or off-line, analyzing extracted execution traces; or it can be used online during operation, potentially steering the application back to a safety region if a property is violated. As a so-called light-weighted formal method, runtime verification bridges the gap between system design and implementation and shorten the distance of software quality assurance between the software testing and model checking and theorem proving. Runtime verification is considered as a highly scalable and automatic technique. Most of current runtime verification research are endeavored on the program context, in other words, on the program side and falls in the implementation level. These applications limited the benefits of runtime verification that bridges the gap among types of applications. With the proliferation of embedded systems and mobile device, dynamically verifying the firmware and mobile apps becomes a new emerging area. Due to the characteristics of runtime verification technique and limitations of the robotics systems, so far, very few research and project are located in the runtime verification on the firmware of embedded systems, which appear in most of robotics systems. Robotics systems are programmed on the firmware and only observed on device. In this paper, the authors first discussed the current runtime verifications on the embedded systems with limitations. After that, a layered runtime verification framework will be presented for the firmware verification. The case study is applied on the commonly recognized educational toolkit – LEGO Mindstorm robotics systems.
30
Rekstin, A., K. Soldatova, Y. Galerkin, and E. Popova. "Verification of a simplified mathematical model of centrifugal compressor stages." E3S Web of Conferences 124 (2019): 01007. http://dx.doi.org/10.1051/e3sconf/201912401007.
Анотація:
To calculate the efficiency of a centrifugal compressor, it is sufficient to know the design parameters and similarity criteria: flow rate coefficient, loading factor, relative hub ratio, Mach number. The effect of the inlet nozzle and the diffuser type is also taken into account. The original simplified model was successfully used for calculation of compressors’ candidates in computer programs of the Universal Modelling Method. Recently, the model has undergone significant revision and been remade. The modernized model is used in the program for primary design of centrifugal compressors. The authors verified the new model, comparing the calculated efficiency with the measured efficiency of several dozens of model stages 21CV family and low flow rate model stages. In total, calculations were carried out for more than thirty model stages. The range of design parameters of analysed model stages is quite wide: flow rate coefficient 0.00564 – 0.0676; loading factor 0.384 – 0.742; hub ratio 0.258 – 0.466.
31
EMERSON, E. ALLEN, KRISTINA D. HAGER, and JAY H. KONIECZKA. "MOLECULAR MODEL CHECKING." International Journal of Foundations of Computer Science 17, no. 04 (August 2006): 733–41. http://dx.doi.org/10.1142/s0129054106004078.
Анотація:
This paper shows how to perform model checking, a technique for automatic program verification, by a DNA algorithm. Our method depends on two ideas. First, Kripke structures can be compactly represented in a DNA substrate, coding each state and each edge by a strand of DNA. Second, satisfaction of temporal eventualities can be achieved through a self-propagating molecular chain reaction.
32
Yamane, Satoshi, Junpei Kobashi, and Kosuke Uemura. "Verification Method of Safety Properties of Embedded Assembly Program by Combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions." Electronics 9, no. 7 (June 27, 2020): 1060. http://dx.doi.org/10.3390/electronics9071060.
Анотація:
Embedded software has properties dependent on hardware (direct operation of address spaces, memory mapped I/O, interruption, etc.). Therefore, demands about the established method of formal verifications corresponding to those properties are increasing from the point of view of shorter development and high reliability. Our study aims at enabling a formal verification with Satisfiability Modulo Theories-Based Bounded Model Checking (SMT-Based BMC) of safety for embedded assembly codes. Our proposed method generates models of assembly codes in detail with the fixed-sized bit-vectors theory. The models generated by our method include interrupts, and the size of the models is reduced using Interrupt Handler Execution Reduction (IHER) technique. In this paper, we have developed the verification method of safety properties of embedded assembly program by combining SMT-Based Bounded Model Checking and Reduction of Interrupt Handler Executions. Moreover, we show the evaluation of our method by experiments using prototype model checker.
33
Leuschel, Michael, Andreas Podelski, C. R. Ramakrishnan, and Ulrich Ultes-Nitsche. "Call for Papers Verification and Computational Logic Special Issue of Theory and Practice of Logic Programming." Theory and Practice of Logic Programming 1, no. 5 (September 2001): 631–32. http://dx.doi.org/10.1017/s1471068401001089.
Анотація:
Submission deadline: January 10, 2002The past decade has seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software systems. One of the methods is to model a hardware or software system as a finite, labelled transition system which is then exhaustively explored to decide whether a given temporal specification holds. Recently, there has been increasing interest in applying logic programming techniques to model checking in particular and verification in general. For example, table-based logic programming can be used as an efficient means of performing explicit model checking. Other research has successfully exploited set-based logic program analysis, constraint logic programming, and logic program transformation techniques.The aim of this special issue is to attract high-quality research papers on the interplay between verification techniques (e.g. model checking, reduction and abstraction) and logic programming techniques (e.g. constraints, abstract interpretation, program transformation).
34
Witkowski, Jakub. "Assessing Selection Mechanisms in Charity Organizations Using Operational Research Methods." Przegląd Statystyczny 64, no. 2 (June 30, 2017): 213–24. http://dx.doi.org/10.5604/01.3001.0014.0803.
Анотація:
The aim of this paper is to assess efficiency of verification policies used in charity organizations. Verification policy can be introduced to ensure that aid is granted only to people who are eligible for it. However, it bears costs for the program’s organizers. The paper provides a theoretical model assessing economic efficiency of ver ification policy using optimization and simulation methods. Depending on characteristics of the program one of three decisions might be optimal: granting aid without verification, granting aid only to positively verified people or not granting aid at all. Therefore, in order to make a decision about introducing verification policy charity organization should analyze parameters of the program such as: average amount of aid, average cost of verification and percentage of people eligible to obtain help in the program.
35
Lee, Jong-gil, and Yung-hea An. "Effects of Design Play Program Using d.School Design Thinking Model on the Creativity of Early Childhood." Korean Association For Learner-Centered Curriculum And Instruction 22, no. 17 (September 15, 2022): 379–96. http://dx.doi.org/10.22251/jlcci.2022.22.17.379.
Анотація:
Objectives This study aims to provide basic data for the field application of design play by verifying the effect on the creativity of infants and developing design play programs using the d.School design thinking model.
Methods To this end, a design play program was developed through related literature analysis, expert consultation, play draft development, and field suitability verification process, and pre-creativity and post-creativity tests were conducted to verify the effectiveness. Covariance analysis (ANCOVA) was performed for the collected data using the SPSS 19.0 Program.
Results First, the developed design play program is as follows. The goals of the program were to develop infants' empathy, develop infants' collaboration, develop infants' problem-solving skills, and develop infants' usefulness skills, and seven activities were selected in connection with the revised Nuri course's life theme. The teaching and learning method was reorganized into six stages, and the evaluation consisted of a formal evaluation of problem-solving ability, expression ability, and attitude as a process-based evaluation and an informal evaluation of infants' language expression, design play results, usefulness. Second, as a result of pre- and post-creativity tests, design play programs were found to have a positive effect on improving children's creativity, and among the sub-elements of creativity, there was a positive effect on the abstraction and sophistication of the title.
Conclusions This study is meaningful in that it suggested the possibility of field application of design play programs using design thinking models through development of design play programs and verification of creativity effects at a time when learning and play support through children's voluntary play is emphasized.
36
FALASCHI, MORENO, and ALICIA VILLANUEVA. "Automatic verification of timed concurrent constraint programs." Theory and Practice of Logic Programming 6, no. 3 (May 2006): 265–300. http://dx.doi.org/10.1017/s1471068406002675.
Анотація:
The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint Programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems. Systems which may have an infinite number of states can be specified in tccp. Model checking is a technique which is able to verify finite-state systems with a huge number of states in an automatic way. In the last years several studies have investigated how to extend model checking techniques to systems with an infinite number of states. In this paper we propose an approach which exploits the computation model of tccp. Constraint based computations allow us to define a methodology for applying a model checking algorithm to (a class of) infinite-state systems. We extend the classical algorithm of model checking for LTL to a specific logic defined for the verification of tccp and to the tccp Structure which we define in this work for modeling the program behavior. We define a restriction on the time in order to get a finite model and then we develop some illustrative examples. To the best of our knowledge this is the first approach that defines a model checking methodology for tccp.
37
Salapatov, V. I. "Order of the description and processing of the program automaton model graph." Mathematical machines and systems 3 (2021): 121–25. http://dx.doi.org/10.34121/1028-9763-2021-3-121-125.
Анотація:
The article considers the method for describing program modeling where predicates are used to create a model in the form of a nondeterministic finite automaton. A format of the description of predicates with the division of their semantic and conditional parts is offered in the paper. Arithmetic operators, parentheses, standard functions, as well as temporal logic operators U and N should be used to describe the content of the predicate. For the logical part of predicates, in addition to their logical functions, it is proposed to use relation operations, arithmetic operators, parentheses and standard functions. The formation of the description of each state of the pro-gram automaton model should be completed by dividing into different branches of the model. To describe the models of parallel programs, the following special states have been introduced: a state-monitor for the access of various processes to shared resources and a state-protocol for the description of independent parallel branches. The model is created in the process of its de-scription, so it does not require further verification. If the description of the model is performed correctly and the optimal algorithm of the future program is selected, such model will fully cor-respond to its description. Unlike MODEL CHECKING technology, which requires verification, it eliminates the need for model verification. The graph of the obtained model is processed by its sequential traversal on all branches with returns to the previous states and subsequent soft-ware implementation. Consecutive traversing should be performed for each branch of the model either to its final state or to the state that has already been processed during the traversal. Model processing includes transmission of the model description into an internal representation for subsequent conversion into a program in the target procedural programming language. In this case all actions in the substantive parts of the predicates, as well as the conditions of the branches in the process of transmission are converted into an internal representation of the pro-gram. This technology provides a direct conversion of the description of the program model in-to the program itself.
38
LEDERER, EDGAR F. A., and ROMEO A. DUMITRESCU. "AUTOMATIC RESULT VERIFICATION BY COMPLETE RUN-TIME CHECKING OF COMPUTATIONS." International Journal of Foundations of Computer Science 12, no. 01 (February 2001): 97–124. http://dx.doi.org/10.1142/s0129054101000424.
Анотація:
Two-Stage Programming (2SP) is an experimental programming language, the first implementation of the Specification-Consistent Coordination Model (SCCM). The SCCM proposes a new, mixed-paradigm (functional/imperative) approach to developing reliable programs based on complete run-time checking of computations with respect to a given specification. A 2SP program consists of a functional specification and an imperative coordination tightly connected to the specification. The coordination maps the specification to an imperative and possibly parallel/distributed program. Normal termination of a 2SP program execution implies the correctness of the computed results with respect to the specification, for that execution. We present the basic feautures of the SCCM/2SP, a new message-spassing system of 2SP with integrated run-time checking, and a larger case study. We show that 2SP provides: functional specifications, specification-consistent imperative coordinations, automatic run-time result verification and error detection, enhanced debugging support, and good efficiency.
39
Jablokow, A. G., J. J. Uicker, and D. A. Turcic. "Verification of Boundary Representations of Solid Models." Journal of Mechanical Design 116, no. 2 (June 1, 1994): 666–68. http://dx.doi.org/10.1115/1.2919430.
Анотація:
Verification of polyhedral boundary representations (B-reps) of solid models through the use of an algorithm is addressed here. The validity conditions for B-rep models are presented in a format which leads directly to a set of verification algorithms. The validity verification algorithms are intended for design automation through execution after each solid modeling operation, after localized geometry modification, on imported object model databases, prior to storage of object models, or prior to execution of an application program on the solid model.
40
Gunawan, Andreas D. M., Bingxin Lu, and Louxin Zhang. "A program for verification of phylogenetic network models." Bioinformatics 32, no. 17 (September 1, 2016): i503—i510. http://dx.doi.org/10.1093/bioinformatics/btw467.
41
Abdulla, Parosh, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. "Verification under Intel-x86 with Persistency." Proceedings of the ACM on Programming Languages 8, PLDI (June 20, 2024): 1189–212. http://dx.doi.org/10.1145/3656425.
Анотація:
The full semantics of the Intel-x86 architecture has been defined by Raad et al in POPL 2022, extending the earlier formalization based on the TSO memory model incorporating persistency. This new semantics involves an intricate combination of the SC, TSO, and PSO models to account for the diverse features of the enlarged instruction set. In this paper we investigate the reachability problem under this semantics, including both its consistency and persistency aspects each of which requires reasoning about unbounded operation reorderings. Our first contribution is to show that reachability under this model can be reduced to reachability under a model without the persistency component. This is achieved by showing that the persistency semantics can be simulated by a finite-state protocol running in parallel with the program. Our second contribution is to prove that reachability under the consistency model of Intel-x86 (even without crashes and persistency) is undecidable. Undecidability is obtained as soon as one thread in the program is allowed to use both TSO variables and two PSO variables. The third contribution is showing that for any fixed bound on the alternation between TSO writes (write-backs), and PSO writes (non-temporal writes), the reachability problem is decidable. This defines a complete parametrized schema for under-approximate analysis that can be used for bug finding.
42
He, Pei, Achun Hu, and Dongqing Xie. "Component-Based Verification Model of Sequential Programs." Journal of Software 10, no. 11 (2015): 1319–26. http://dx.doi.org/10.17706/jsw.10.11.1319-1326.
43
Chang, Bao Rong, Hsiu-Fen Tsai, and Po-Wen Su. "Applying Code Transform Model to Newly Generated Program for Improving Execution Performance." Scientific Programming 2021 (February 1, 2021): 1–21. http://dx.doi.org/10.1155/2021/6691010.
Анотація:
The existing programs inside the voice assistant machine prompt human-machine interaction in response to a request from a user. However, the crucial problem is that the machine often may not give a proper answer to the user or cannot work out the existing program execution efficiently. Therefore, this study proposes a novel transform method to replace the existing programs (called sample programs in this paper) inside the machine with newly generated programs through code transform model GPT-2 that can reasonably solve the problem mentioned above. In essence, this paper introduces a theoretical estimation in statistics to infer at least a number of generated programs as required so as to guarantee that the best one can be found within them. In addition, the proposed approach not only imitates a voice assistant system with filtering redundant keywords or adding new keywords to complete keyword retrieval in semantic database but also checks code similarity and verifies the conformity of the executive outputs between sample programs and newly generated programs. According to code checking and program output verification, the processes can expedite transform operations efficiently by removing the redundant generated programs and finding the best-performing generated program. As a result, the newly generated programs outperform the sample programs because the proposed approach reduces the number of code lines by 32.71% and lowers the program execution time by 24.34%, which is of great significance.
44
UNNO, HIROSHI, NAOSHI TABUCHI, and NAOKI KOBAYASHI. "Verification of tree-processing programs via higher-order mode checking." Mathematical Structures in Computer Science 25, no. 4 (November 10, 2014): 841–66. http://dx.doi.org/10.1017/s0960129513000054.
Анотація:
We propose a new method to verify that a higher-order, tree-processing functional program conforms to an input/output specification. Our method reduces the verification problem to multiple verification problems for higher-order multi-tree transducers, which are then transformed into higher-order recursion schemes and model-checked. Unlike previous methods, our new method can deal with arbitrary higher-order functional programs manipulating algebraic data structures, as long as certain invariants on intermediate data structures are provided by a programmer. We have proved the soundness of the method and implemented a prototype verifier.
45
Kobayashi, Naoki, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada. "HFL(Z) Validity Checking for Automated Program Verification." Proceedings of the ACM on Programming Languages 7, POPL (January 9, 2023): 154–84. http://dx.doi.org/10.1145/3571199.
Анотація:
We propose an automated method for checking the validity of a formula of HFL(Z), a higher-order logic with fixpoint operators and integers. Combined with Kobayashi et al.'s reduction from higher-order program verification to HFL(Z) validity checking, our method yields a fully automated, uniform verification method for arbitrary temporal properties of higher-order functional programs expressible in the modal mu-calculus, including termination, non-termination, fair termination, fair non-termination, and also branching-time properties. We have implemented our method and obtained promising experimental results.
46
Gong, Wei, and Jun Wei Jia. "Comparison of Model Checking Tools." Advanced Materials Research 659 (January 2013): 181–85. http://dx.doi.org/10.4028/www.scientific.net/amr.659.181.
Анотація:
Model Checking is a method for verification. The model will be checked until the specification of it is proved or disproved. With the rising complexity of big models, there are non-checkable cases, in which cases the problem can be analyzed by some models, for example, bounded Model Checking means to analyze the model until a defined time or depth. The verification happens automatically. The programs for doing this are called Model Checking Tools or Model Checker. Model Checking are used in both software and hardware verification. It is an inherent part of hardware verification, whereas it is less used in the software verification.
47
Kherbouche, Meriem, Galena Pisoni, and Bálint Molnár. "Model to Program and Blockchain Approaches for Business Processes and Workflows in Finance." Applied System Innovation 5, no. 1 (January 4, 2022): 10. http://dx.doi.org/10.3390/asi5010010.
Анотація:
Business process modeling and verification have become an essential way to control and assure organizational evolution. We overview the opportunities for the application of blockchain in Business Process Management and Modeling in Finance and we focus on in-depth analysis of claim process in insurance as a use case. We investigate the utilization of blockchain technology for model checking of Workflow, Business Processes to ensure consistency, integrity, and security in a dynamically changing business environment. We create a UML profile for the blockchain, then we combine it with a UML activity diagram followed by a verification using Petri nets to guarantee a distributed computing system and scalable with mutable data. Our paper creates a unified picture of the approaches towards business processes modeling used in the financial industry organized around the set of premises intending to develop a future research agenda for blockchain business process modeling, specifically for the financial industry domain.
48
Steingartner, William, and Valerie Novitzká. "Categorical model of structural operational semantics for imperative language." Journal of information and organizational sciences 40, no. 2 (December 9, 2016): 203–19. http://dx.doi.org/10.31341/jios.40.2.3.
Анотація:
Definition of programming languages consists of the formal definition of syntax and semantics. One of the most popular semantic methods used in various stages of software engineering is structural operational semantics. It describes program behavior in the form of state changes after execution of elementary steps of program. This feature makes structural operational semantics useful for implementation of programming languages and also for verification purposes. In our paper we present a new approach to structural operational semantics. We model behavior of programs in category of states, where objects are states, an abstraction of computer memory and morphisms model state changes, execution of a program in elementary steps. The advantage of using categorical model is its exact mathematical structure with many useful proved properties and its graphical illustration of program behavior as a path, i.e. a composition of morphisms. Our approach is able to accentuate dynamics of structural operational semantics. For simplicity, we assume that data are intuitively typed. Visualization and facility of our model is not only a new model of structural operational semantics of imperative programming languages but it can also serve for education purposes.
49
Belardinelli, Francesco, Ioana Boureanu, Vadim Malvone, and Fortunat Rajaona. "Automatically Verifying Expressive Epistemic Properties of Programs." Proceedings of the AAAI Conference on Artificial Intelligence 37, no. 5 (June 26, 2023): 6245–52. http://dx.doi.org/10.1609/aaai.v37i5.25769.
Анотація:
We propose a new approach to the verification of epistemic properties of programmes. First, we introduce the new ``program-epistemic'' logic L_PK, which is strictly richer and more general than similar formalisms appearing in the literature. To solve the verification problem in an efficient way, we introduce a translation from our language L_PK into first-order logic. Then, we show and prove correct a reduction from the model checking problem for program-epistemic formulas to the satisfiability of their first-order translation. Both our logic and our translation can handle richer specification w.r.t. the state of the art, allowing us to express the knowledge of agents about facts pertaining to programs (i.e., agents' knowledge before a program is executed as well as after is has been executed). Furthermore, we implement our translation in Haskell in a general way (i.e., independently of the programs in the logical statements), and we use existing SMT-solvers to check satisfaction of L_PK formulas on a benchmark example in the AI/agency field.
50
Tan, Lanfang, Qingping Tan, Jianjun Xu, and Huiping Zhou. "Formal verification of signature-monitoring mechanisms by model checking." Computer Science and Information Systems 9, no. 4 (2012): 1431–51. http://dx.doi.org/10.2298/csis120218056t.
Анотація:
In recent decades, reliability in the presence of transient faults has been a significant problem. To mitigate the effects of transient faults, fault-tolerant techniques are proposed. However, validating the effectiveness of fault-tolerant techniques is another problem. In this paper, we present an original approach to evaluate the effectiveness of signature-monitoring mechanisms. The approach is based on model-checking principles. First, the fault tolerant model is proposed using step-operational semantics. Second, the fault model is refined into a state transition system that is translated into the input program of the symbolic model checker NuSMV. Using NuSMV, two reprehensive signature-monitoring algorithms are verified. The approach avoids the state space explosion problem and the verification was completed with practical time. The verification results reveal some undetected errors, which have not been previously observed.