A Vulnerability Model Construction Method Based on Chemical Abstract Machine

It is difficult to formalize the causes of vulnerability, and there is no effective model to reveal the causes and characteristics of vulnerability. In this paper, a vulnerability model construction method is proposed to realize the description of vulnerability attribute and the construction of a vulnerability model. A vulnerability model based on chemical abstract machine（CHAM） is constructed to realize the CHAM description of vulnerability model, and the framework of vulnerability model is also discussed. Case study is carried out to verify the feasibility and effectiveness of the proposed model. In addition, a prototype system is also designed and implemented based on the proposed vulnerability model. Experimental results show that the proposed model is more effective than other methods in the detection of software vulnerabilities.

Verifying the accuracy of interlocking tables for railway signalling systems using abstract state machines

Railway transportation system is a critical sector where design methods and techniques are defined by international standards in order to reduce possible risks to an acceptable minimum level. CENELEC 50128 strongly recommends the utilization of finite state machines during system modelling stage and formal proof methods during the verifi- cation and testing stages of control algorithms. Due to the high importance of interlocking table at the design state of a sig- nalization system, the modelling and verification of inter- locking tables are examined in this work. For this purpose, abstract state machines are used as a modelling tool. The developed models have been performed in a generalized structure such that the model control can be done automatically for the interlocking systems. In this study, NuSMV is used at the verification state. Also, the consistency of the developed models has been supervised through fault injection. The developed models and software components are applied on a real railway station operated by Metro Istanbul Co.

HEST: A Hybrid-Language-Based Expert System Tool

HEST is a practical integrated expert system tool. Its basis is a knowledge programming language FFLL, characterized by a combination of fuzzy logic and function paradigms. The tool integrates alot of important knowledge processing capabilities such as fuzzy reasoning, function computation, knowledge compilation and explanation, knowledge base maintenance, as well as practical programming functions, e.g., editing, filing, compiling, module imbedding, etc., constructing, a user--friendly knowledge application environment, HEST can enable expert system development in various domaills quickly and easily.This paper gives an outline of the design and implementation of HEST.

Remolding Diversified Objects in Ada95: Toward A Object Pattern

Ada provides full capacities of supporting object orientation, but the diversified objects patterned in Ada are so intricate that Ada95's aim would be demolished. In order to complement the disfigurement that Ada does lack for a pristine notion of class, this paper presents a remolded object pattern known as A object, an Ada based class description language A ObjAda aiming at support for A object pattern and the related approach for key algorithms and implementation. In consequent, A ObjAda hereby promotes Ada with highlighted object orientation, which not only effectively exploits the capacities in Ada95, but also rationally hides befuddling concepts from Ada95.

Formal Verification of TASM Models by Translating into UPPAAL

Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. Formal verification of TASM model can be fulfilled through model checking activities by translating into UPPAAL. Firstly, the translational semantics from TASM to UPPAAL is presented through atlas transformation language(ATL). Secondly, the implementation of the proposed model transformation tool TASM2UPPAAL is provided. Finally, a case study is given to illustrate the automatic transformation from TASM model to UPPAAL model.

AADL2TASM: a Verification and Analysis Tool for AADL Models

Architecture analysis and design language (AADL) is an architecture description language standard for embedded real-time systems and it is widely used in safety-critical applications. For facilitating verification and analysis, model transformation is one of the methods. A synchronous subset of AADL and a general methodology for translating the AADL subset into timed abstract state machine (TASM) were studied . Based on the atlas transformation language (ATL) framework, the associated translating tool AADL2TASM was implemented by defining the meta-model of both AADL and TASM, and the ATL transformation rules. A case study with property verification of the AADL model was also presented for validating the tool.

Optimized Parallel Execution of Declarative Programs on Distributed Memory Multiprocessors

In this paper,we focus on the compiling implementation of parallel logic language PARLOG and functional language ML on distributed memory multiprocessors.Under the graph rewriting framework, a Heterogeneous Parallel Graph Rewriting Execution Model(HPGREM)is presented firstly.Then based on HPGREM,a parallel abstract machine PAM/TGR is described.Furthermore,several optimizing compilation schemes for executing declarative programs on transputer array are proposed. The performance statistics on a transputer array demonstrate the effectiveness of our model,parallel ab- stract machine,optimizing compilation strategies and compiler.

An Buffer Overflow Automatic Detection Method Based on Operation Semantic

Buffer overflow is the most dangerous attack method that can be exploited. According to the statistics of Computer Emergency Readiness Team （ CERT ）, buffer overflow accounts for 50% of the current software vulnerabilities, and this ratio is going up. Considering a subset of C language, Mini C, this paper presents an abstract machine model that can realire buffer overflow detection, which is based on operation semantic. Thus the research on buffer overflow detection can be built on strict descriptions of operation semantic. Not only the correctness can be assured, but also the system can be realized and extended easily.

New Semantic Model for Authentication Protocols in ASMs

A new semantic model in Abstract State Model (ASM) for authentication protocols is presented. It highlights the Woo-Lam's ideas for authentication, which is the strongest one in Lowe's definition hierarchy for entity authentication. Apart from the flexible and natural features in forming and analyzing protocols inherited from ASM, the model defines both authentication and secrecy properties explicitly in first order sentences as invariants. The process of proving security properties with respect to an authentication protocol blends the correctness and secrecy properties together to avoid the potential flaws which may happen when treated separately. The security of revised Helsinki protocol is shown as a case study. The new model is different from the previous ones in ASMs.

A Modeling Language Based on UML for Modeling Simulation Testing System of Avionic Software

With direct expression of individual application domain patterns and ideas,domain-specific modeling language（DSML） is more and more frequently used to build models instead of using a combination of one or more general constructs.Based on the profile mechanism of unified modeling language（UML） 2.2,a kind of DSML is presented to model simulation testing systems of avionic software（STSAS）.To define the syntax,semantics and notions of the DSML,the domain model of the STSAS from which we generalize the domain concepts and relationships among these concepts is given,and then,the domain model is mapped into a UML meta-model,named UML-STSAS profile.Assuming a flight control system（FCS） as system under test（SUT）,we design the relevant STSAS.The results indicate that extending UML to the simulation testing domain can effectively and precisely model STSAS.