scholarly journals Constraint-based automatic verification of abstract models of multithreaded programs

2007 ◽  
Vol 7 (1-2) ◽  
pp. 67-91 ◽  
Author(s):  
GIORGIO DELZANNO
Keyword(s):  
Automated Verification ◽  
Infinite Domain ◽  
Verification Method ◽  
Low Level ◽  
Multithreaded Programs ◽  
Unbounded Control ◽  
Finite State ◽  
High Level ◽  
Syntactic Restrictions ◽  
Local Variable

AbstractWe present a technique for the automated verification of abstract models of multithreaded programs providing fresh name generation, name mobility, and unbounded control. As high level specification language we adopt here an extension of communication finite-state machines with local variables ranging over an infinite name domain, called TDL programs. Communication machines have been proved very effective for representing communication protocols as well as for representing abstractions of multithreaded software. The verification method that we propose is based on the encoding of TDL programs into a low level language based on multiset rewriting and constraints that can be viewed as an extension of Petri Nets. By means of this encoding, the symbolic verification procedure developed for the low level language in our previous work can now be applied to TDL programs. Furthermore, the encoding allows us to isolate a decidable class of verification problems for TDL programs that still provide fresh name generation, name mobility, and unbounded control. Our syntactic restrictions are in fact defined on the internal structure of threads: In order to obtain a complete and terminating method, threads are only allowed to have at most one local variable (ranging over an infinite domain of names).

Powered Ankle-Foot Prostheses: A Survey on Sensing Systems and Control Strategies

2019 ◽  
Author(s):  
Erik Chumacero-Polanco ◽  
James Yang
Keyword(s):  
Control Strategies ◽  
Level Control ◽  
Low Level ◽  
Kinetic Information ◽  
Sensing Systems ◽  
Systems And Control ◽  
Finite State ◽  
High Level ◽  
And Control

Abstract People who have suffered a transtibial amputation show diminished ambulation and impaired quality of life. Powered ankle foot prostheses (AFP) are used to recover some mobility of transtibial amputees (TTAs). Powered AFP is an emerging technology that has great potential to improve the quality of life of TTAs with important avenues for research and development in different fields. This paper presents a survey on sensing systems and control strategies applied to powered AFPs. Sensing kinematic and kinetic information in powered AFPs is critical for control. Ankle angle position is commonly obtained via potentiometers and encoders directly installed on the joint, velocities can be estimated using numerical differentiators, and accelerations are normally obtained via inertial measurement units (IMUs). On the other hand, kinetic information is usually obtained via strain gauges and torque sensors. On the other hand, control strategies are classified as high- and low-level control. The high-level control sets the torque or position references based on pattern generators, user’s intent of motion recognition, or finite-state machine. The low-level control usually consists of linear controllers that drive the ankle’s joint position, velocity, or torque to follow an imposed reference signal. The most widely used control strategy is the one based on finite-state machines for the high-level control combined with a proportional-derivative torque control for low-level. Most designs have been experimentally assessed with acceptable results in terms of walking speed. However, some drawbacks related to powered AFP’s weight and autonomy remain to be overcome. Future research should be focused on reducing powered AFP size and weight, increasing energy efficiency, and improving both the high- and the low-level controllers in terms of efficiency and performance.

Implementation of robotic ankle–foot orthosis with an impedance-based assist-as-needed control strategy

2021 ◽  
pp. 1-40
Author(s):  
Bing Chen ◽  
Bin Zi ◽  
Bin Zhou ◽  
Zhengyu Wang
Keyword(s):  
Level Control ◽  
Ankle Foot Orthosis ◽  
Low Level ◽  
Ankle Impedance ◽  
Torque Generation ◽  
Ankle Rehabilitation ◽  
Finite State ◽  
Proportional Derivative Controller ◽  
High Level ◽  
Foot Orthosis

Abstract In this paper, a robotic ankle–foot orthosis (AFO) is developed for individuals with a paretic ankle, and an impedance-based assist-as-needed controller is designed for the robotic AFO to provide adaptive assistance. First, a description of the robotic AFO hardware design is presented. Next, the design of the finite state machine is introduced, followed by an introduction to the modelling of the robotic AFO. Additionally, the control of the robotic AFO is presented. An impedance-based high-level controller that is composed of an ankle impedance based torque generation controller and an impedance controller is designed for the high-level control. A compensated low-level controller that is composed of a braking controller and a proportional-derivative controller with a compensation part is designed for the low-level control. Finally, a pilot study is conducted, and the experimental results demonstrate that with the proposed control algorithm, the robotic AFO has the potential for ankle rehabilitation by providing adaptive assistance. In the assisted condition with a high level of assistance, reductions of 8% and 20.1% of the root mean square of the tibialis anterior and lateral soleus activities are observed, respectively.

scholarly journals Doppelganger Obfuscation — Exploring theDefensive and Offensive Aspects of Hardware Camouflaging

2020 ◽  
pp. 82-108
Author(s):  
Max Hoffmann ◽  
Christof Paar
Keyword(s):  
Reverse Engineering ◽  
Low Level ◽  
Reverse Engineer ◽  
Finite State ◽  
Key Leakage ◽  
The One ◽  
High Level ◽  
Generic Design ◽  
Control Modules ◽  
First Time

Hardware obfuscation is widely used in practice to counteract reverse engineering. In recent years, low-level obfuscation via camouflaged gates has been increasingly discussed in the scientific community and industry. In contrast to classical high-level obfuscation, such gates result in recovery of an erroneous netlist. This technology has so far been regarded as a purely defensive tool. We show that low-level obfuscation is in fact a double-edged sword that can also enable stealthy malicious functionalities.In this work, we present Doppelganger, the first generic design-level obfuscation technique that is based on low-level camouflaging. Doppelganger obstructs central control modules of digital designs, e.g., Finite State Machines (FSMs) or bus controllers, resulting in two different design functionalities: an apparent one that is recovered during reverse engineering and the actual one that is executed during operation. Notably, both functionalities are under the designer’s control.In two case studies, we apply Doppelganger to a universal cryptographic coprocessor. First, we show the defensive capabilities by presenting the reverse engineer with a different mode of operation than the one that is actually executed. Then, for the first time, we demonstrate the considerable threat potential of low-level obfuscation. We show how an invisible, remotely exploitable key-leakage Trojan can be injected into the same cryptographic coprocessor just through obfuscation. In both applications of Doppelganger, the resulting design size is indistinguishable from that of an unobfuscated design, depending on the choice of encodings.

Teknik Data Mining Dalam Clustering Produksi Susu Segar Di Indonesia Dengan Algoritma K-Means

2019 ◽  
Vol 1 (1) ◽  
pp. 31-39
Author(s):  
Ilham Safitra Damanik ◽  
Sundari Retno Andani ◽  
Dedi Sehendro
Keyword(s):  
Data Mining ◽  
Milk Production ◽  
Clustering Algorithm ◽  
Clustering Method ◽  
Data Mining Techniques ◽  
Low Level ◽  
Fresh Milk ◽  
Nutritional Needs ◽  
High Level ◽  
Level Cluster

Milk is an important intake to meet nutritional needs. Both consumed by children, and adults. Indonesia has many producers of fresh milk, but it is not sufficient for national milk needs. Data mining is a science in the field of computers that is widely used in research. one of the data mining techniques is Clustering. Clustering is a method by grouping data. The Clustering method will be more optimal if you use a lot of data. Data to be used are provincial data in Indonesia from 2000 to 2017 obtained from the Central Statistics Agency. The results of this study are in Clusters based on 2 milk-producing groups, namely high-dairy producers and low-milk producing regions. From 27 data on fresh milk production in Indonesia, two high-level provinces can be obtained, namely: West Java and East Java. And 25 others were added in 7 provinces which did not follow the calculation of the K-Means Clustering Algorithm, including in the low level cluster.

Determinants of Abuse of the Bodies of the Dead

2019 ◽  
pp. 71-77
Author(s):  
Margarita Khomyakova
Keyword(s):  
Low Income ◽  
Criminal Code ◽  
Value Judgments ◽  
Legal Norms ◽  
Low Level ◽  
Medical Institutions ◽  
Specific Object ◽  
The Subject ◽  
The Dead ◽  
High Level

The author analyzes definitions of the concepts of determinants of crime given by various scientists and offers her definition. In this study, determinants of crime are understood as a set of its causes, the circumstances that contribute committing them, as well as the dynamics of crime. It is noted that the Russian legislator in Article 244 of the Criminal Code defines the object of this criminal assault as public morality. Despite the use of evaluative concepts both in the disposition of this norm and in determining the specific object of a given crime, the position of criminologists is unequivocal: crimes of this kind are immoral and are in irreconcilable conflict with generally accepted moral and legal norms. In the paper, some views are considered with regard to making value judgments which could hardly apply to legal norms. According to the author, the reasons for abuse of the bodies of the dead include economic problems of the subject of a crime, a low level of culture and legal awareness; this list is not exhaustive. The main circumstances that contribute committing abuse of the bodies of the dead and their burial places are the following: low income and unemployment, low level of criminological prevention, poor maintenance and protection of medical institutions and cemeteries due to underperformance of state and municipal bodies. The list of circumstances is also open-ended. Due to some factors, including a high level of latency, it is not possible to reflect the dynamics of such crimes objectively. At the same time, identification of the determinants of abuse of the bodies of the dead will reduce the number of such crimes.

scholarly journals EXPRESS: Marketers Project Their Personal Preferences onto Consumers: Overcoming the Threat of Egocentric Decision Making

2021 ◽  
pp. 002224372199837
Author(s):  
Walter Herzog ◽  
Johannes D. Hattula ◽  
Darren W. Dahl
Keyword(s):  
Decision Making ◽  
Consumer Preferences ◽  
Research Question ◽  
Pilot Studies ◽  
Low Level ◽  
Marketing Managers ◽  
False Consensus Effect ◽  
False Consensus ◽  
High Level

This research explores how marketing managers can avoid the so-called false consensus effect—the egocentric tendency to project personal preferences onto consumers. Two pilot studies were conducted to provide evidence for the managerial importance of this research question and to explore how marketing managers attempt to avoid false consensus effects in practice. The results suggest that the debiasing tactic most frequently used by marketers is to suppress their personal preferences when predicting consumer preferences. Four subsequent studies show that, ironically, this debiasing tactic can backfire and increase managers’ susceptibility to the false consensus effect. Specifically, the results suggest that these backfire effects are most likely to occur for managers with a low level of preference certainty. In contrast, the results imply that preference suppression does not backfire but instead decreases false consensus effects for managers with a high level of preference certainty. Finally, the studies explore the mechanism behind these results and show how managers can ultimately avoid false consensus effects—regardless of their level of preference certainty and without risking backfire effects.

Exploring The Effect of Visual Information Degradation on Human Perception and Performance In A Human-Telerobot System

2020 ◽  
Vol 64 (1) ◽  
pp. 1302-1307
Author(s):  
Richard Stone ◽  
Minglu Wang ◽  
Thomas Schnieders ◽  
Esraa Abdelall
Keyword(s):  
Visual Information ◽  
Human Perception ◽  
Low Level ◽  
Hit Rate ◽  
Word Level ◽  
Level Of Automation ◽  
Significant Difference ◽  
Human Operators ◽  
And Performance ◽  
High Level

Human-robotic interaction system are increasingly becoming integrated into industrial, commercial and emergency service agencies. It is critical that human operators understand and trust automation when these systems support and even make important decisions. The following study focused on human-in-loop telerobotic system performing a reconnaissance operation. Twenty-four subjects were divided into groups based on level of automation (Low-Level Automation (LLA), and High-Level Automation (HLA)). Results indicated a significant difference between low and high word level of control in hit rate when permanent error occurred. In the LLA group, the type of error had a significant effect on the hit rate. In general, the high level of automation was better than the low level of automation, especially if it was more reliable, suggesting that subjects in the HLA group could rely on the automatic implementation to perform the task more effectively and more accurately.

scholarly journals The high-level benefits of low-level sandboxing

2020 ◽  
Vol 4 (POPL) ◽  
pp. 1-32 ◽  
Author(s):  
Michael Sammler ◽  
Deepak Garg ◽  
Derek Dreyer ◽  
Tadeusz Litak
Keyword(s):  
Low Level ◽  
High Level

Urban network of China from the perspective of population mobility: Three-dimensional co-occurrence of nodes and links

2021 ◽  
pp. 0308518X2199781
Author(s):  
Xinyue Luo ◽  
Mingxing Chen
Keyword(s):  
Three Dimensional ◽  
Geographical Distance ◽  
Two Dimensional ◽  
Population Mobility ◽  
Urban Network ◽  
Urban Networks ◽  
Low Level ◽  
Medium Level ◽  
High Level ◽  
External Connections

The nodes and links in urban networks are usually presented in a two-dimensional(2D) view. The co-occurrence of nodes and links can also be realized from a three-dimensional(3D) perspective to make the characteristics of urban network more intuitively revealed. Our result shows that the external connections of high-level cities are mainly affected by the level of cities(nodes) and less affected by geographical distance, while medium-level cities are affected by the interaction of the level of cities(nodes) and geographical distance. The external connections of low-level cities are greatly restricted by geographical distance.

Sign in / Sign up

Export Citation Format

Share Document