Model Extraction and Reliability Verification on SOCKET Program

2012 ◽  
Vol 616-618 ◽  
pp. 2055-2059
Author(s):  
Min Luo
Keyword(s):  
Program Analysis ◽  
Formal Method ◽  
Sequence Structure ◽  
Communication Program ◽  
Function Call ◽  
Extraction Algorithm ◽  
Run Time ◽  
Analysis System ◽  
High Level ◽  
Call Sequence

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.

Alchemy: Distributed financial quantitative analysis system with high‐level programming model

2021 ◽  
Author(s):  
Rong Gu ◽  
Zhixiang Zhang ◽  
Zhihao Xu ◽  
Zhaokang Wang ◽  
Kai Zhang ◽  
...  
Keyword(s):  
Quantitative Analysis ◽  
Programming Model ◽  
Analysis System ◽  
High Level

Design for Assembly Evaluation of Orientation Difficulty Features

1992 ◽  
Author(s):  
Robert H. Sturges ◽  
Jui-Te Yang
Keyword(s):  
Geometric Modeling ◽  
Boundary Representation ◽  
Design For Assembly ◽  
Assembly Process ◽  
Assembly Evaluation ◽  
Index Of Difficulty ◽  
Analysis System ◽  
Time Required ◽  
High Level ◽  
Geometric Modeling System

Abstract In support of the effort to bring downstream issues to the attention of the designer as parts take shape, an analysis system is being built to extract certain features relevant to the assembly process, such as the dimension, shape, and symmetry of an object. These features can be applied to a model during the downstream process to evaluate handling and assemblability. In this paper, we will focus on the acquisition phase of the assembly process and employ a Design for Assembly (DFA) evaluation to quantify factors in this process. The capabilities of a non-homogeneous, non-manifold boundary representation geometric modeling system are used with an Index of Difficulty (ID) that represents the dexterity and time required to assemble a product. A series of algorithms based on the high-level abstractions of loop and link are developed to extract features that are difficult to orient, which is one of the DFA criteria. Examples for testing the robustness of the algorithms are given. Problems related to nearly symmetric outlines are also discussed.

scholarly journals A Runtime System for XML Transformations in Java

2004 ◽  
Vol 11 (33) ◽  
Author(s):  
Aske Simon Christensen ◽  
Christian Kirkegaard ◽  
Anders Møller
Keyword(s):  
Static Analysis ◽  
Programming Language ◽  
Program Analysis ◽  
Companion Paper ◽  
General Purpose ◽  
Runtime System ◽  
Xml Documents ◽  
Level Data ◽  
High Level ◽  
The Given

We show that it is possible to extend a general-purpose programming language with a convenient high-level data-type for manipulating XML documents while permitting (1) precise static analysis for guaranteeing validity of the constructed XML documents relative to the given DTD schemas, and (2) a runtime system where the operations can be performed efficiently. The system, named Xact, is based on a notion of immutable XML templates and uses XPath for deconstructing documents. A companion paper presents the program analysis; this paper focuses on the efficient runtime representation.

scholarly journals The program of communicative and personal development of primary schoolchildren within the framework of an innovative university-school partnership: Evaluation of the effectiveness

2021 ◽  
Vol 11 (4) ◽  
pp. 7-32
Author(s):  
Yulia Valerievna Batenova ◽  
◽  
Marina Yuryevna Buslaeva ◽  
Marina Nikolaevna Tereshchenko ◽  
Nadezhda Borisovna Novikova ◽  
...  
Keyword(s):  
Personal Development ◽  
Validity And Reliability ◽  
Communicative Development ◽  
Communication Program ◽  
Primary Schoolchildren ◽  
Research Findings ◽  
School Partnership ◽  
Methodological Principles ◽  
Level Of Understanding ◽  
High Level

Introduction. The article addresses the problem of primary schoolchildren’s communicative and personal development within the frameworks of an innovative university-school partnership. The purpose of the article is to evaluate the effectiveness of the program aimed at communicative and personal development of primary schoolchildren and to identify psychological and educational factors contributing to its implementation. Materials and Methods. The research follows learner-centered, semiotic, and hermeneutic approaches. In order to assess communicative development of primary schoolchildren, the following empirical methods were used: G. A. Zuckerman’s ‘Mittens’ inventory, O. G. Mishanova’s ‘Polite words’ inventory, G. A. Zuckerman’s ‘Dictation Pattern’ inventory, the ‘Brothers and Sisters’ method (modified samples of Zh. Piaget). The study involved 50 primary schoolchildren and 4 primary school teachers. To analyze the empirical data and evaluate the dynamics, the Wilcoxon T-test was used, which ensures the validity and reliability of research findings. Results. The article analyzes and summarizes the experience of currently available programs aimed at social and communicative development of primary schoolchildren. The authors have developed a program enhancing primary schoolchildren’s communicative development, theoretically justified and implemented it. The explanatory and heuristic potential of methodological principles and approaches to solving this problem has been revealed. The authors describe an educational technology called ‘a hermeneutic circle’ and illustrate it by means of a text analyzes focusing on its expediency, relevance, and communicative significance for effective cognition of the language essence and training communicative skills. The research findings indicate the effectiveness of the program called ‘Culture of speech and ethics of communication’ in the communicative and personal development of primary schoolchildren in four areas: communication as cooperation; communication as management; communication as interiorization; communication as interaction. Relying on these directions, the authors have identified and described the following parameters of the integral communicative and personal development: the level of dialogic communication, the level of communication ethics, the level of communication productivity, the level of understanding of the other participants. Conclusions. The article concludes that the implementation of ‘Culture of speech and ethics of communication’ program and creating a psychologically beneficial learning environment have led to a high level of communicative and personal development of primary schoolchildren who consider language as a cultural, ethical, and aesthetic value.

Crankshaft Stress Analysis—Combination of Finite Element and Classical Analysis Techniques

1990 ◽  
Vol 112 (3) ◽  
pp. 268-275 ◽  
Author(s):  
A. R. Heath ◽  
P. M. McNamara
Keyword(s):  
Stress Analysis ◽  
Concept Design ◽  
Low Friction ◽  
Failure Investigation ◽  
Engine Design ◽  
Computer Based ◽  
Analysis System ◽  
High Level ◽  
Engine Components ◽  
Oil Films

The conflicting legislative and customer pressures on engine design, for example, combining low friction and a high level of refinement, require sophisticated tools if competitive designs are to be realized. This is particularly true of crankshafts, probably the most analyzed of all engine components. This paper describes the hierarchy of methods used for crankshaft stress analysis with case studies. A computer-based analysis system is described that combines FE and classical methods to allow optimized designs to be produced efficiently. At the lowest level simplified classical techniques are integrated into the CAD-based design process. These methods give the rapid feedback necessary to perform concept design iterations. Various levels of FE analysis are available to carry out more detailed analyses of the crankshaft. The FE studies may feed information to or take information from the classical methods. At the highest level a method for including the load sharing effects of the flexible crankshaft within a flexible block interconnected by nonlinear oil films is described. This method includes the FE modeling of the complete crankshaft and the consideration of its stress field throughout an engine cycle. Fatigue assessment is performed to calculate the distribution of fatigue safety factor on the surface of the crankshaft. This level of analysis can be used for failure investigation, or detailed design optimization and verification. The method is compatible with those used for vibration and oil film analysis.

Precision of a Novel Vertebral Motion Analysis System: Preliminary Results

2012 ◽  
Author(s):  
Matthew S. Yeager ◽  
Daniel J. Cook ◽  
Boyle C. Cheng
Keyword(s):  
Muscle Activation ◽  
X Rays ◽  
Current Standard ◽  
Body Depth ◽  
Standard Of Practice ◽  
Static Images ◽  
Magnetic Resonance Imaging Mri ◽  
Analysis System ◽  
High Level ◽  
Relative Change

Imaging modalities such as X-Ray, computerized tomography (CT), magnetic resonance imaging (MRI), and bone scan have all become essential to the evaluation of bone and soft tissue in patients with back pain. All techniques provide valuable static images of the spine, yet lack the capability of providing detailed information about spinal motion. Dynamic end-range x-rays, the standard in assessment of range of motion and vertebral translation, are taken at the patient’s maximum voluntary bending angle in flexion and extension (FE) and/or lateral bending (LB). The current standard of practice is to measure, with ruler and protractor, the relative change between adjacent vertebrae at each bending extreme. The resulting rotational or translational values are then expressed as the intervertebral angle (IVA) or as a percentage of vertebral body depth, respectively. This method, however, is subject to a high level of patient, imaging site, and observer related variability, in the form of uncontrolled bending angles, disparities in equipment and practices, and manual image analysis. An additional limitation of static imagery is the inability to assess motion in the spine as it traverses between end ranges. This information may expose motion abnormalities that occur mid-range that might otherwise be missed by clinicians. Lastly, motion of the spine may present differently in weighted and un-weighted positions. Effects of muscle activation and gravitational forces are not accounted for by current standards.

A Formal Method for Optimal High-Level Casting of Heterogeneous Fixed-Point Adders and Subtractors

2015 ◽  
Vol 34 (1) ◽  
pp. 52-62 ◽  
Author(s):  
Roberto Sierra ◽  
Carlos Carreras ◽  
Gabriel Caffarena ◽  
Carlos A. Lopez Bario
Keyword(s):  
Fixed Point ◽  
Formal Method ◽  
High Level

Simulation of Boat Launching and Hoisting in a Seaway

2008 ◽  
Author(s):  
Heinrich So¨ding ◽  
Michael Reppenhagen
Keyword(s):  
Water Surface ◽  
Simulation System ◽  
Software Simulation ◽  
Small Boat ◽  
Run Time ◽  
High Level

For modeling the launching and hoisting of a small boat from/to a ship advancing in moderate seaway a software simulation system was developed. Its purpose is to test various procedures and the necessary equipment for such maneuvers. The software will be extended further as a ’federation’ within a ’high-level program architecture’ (HLA) using the commercial ’run-time infrastructure’ (RTI). It comprises a visualization of the water surface, the frigate, the boat and the cables connecting both vehicles during part of the maneuvers.

Sign in / Sign up

Export Citation Format

Share Document