Search results for: Algebraic Specification

Authors: Yun Bai

Abstract:

As a security mechanism, authorization is to provide access control to the system resources according to the polices and rules specified by the security strategies. Either by update or in the initial specification, conflicts in authorization is an issue needs to be solved. In this paper, we propose a new approach to solve conflict by using prioritized logic programs and discuss the uniqueness of its answer set. Addressing conflict resolution from logic programming viewpoint and the uniqueness analysis of the answer set provide a novel, efficient approach for authorization conflict resolution.

Keywords: authorization, formal specification, conflict resolution, prioritized logic program.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1487

Authors: Chahid K. Ghaddar

Abstract:

The spreadsheet engine is exploited via a non-conventional mechanism to enable novel worksheet solver functions for computational calculus. The solver functions bypass inherent restrictions on built-in math and user defined functions by taking variable formulas as a new type of argument while retaining purity and recursion properties. The enabling mechanism permits integration of numerical algorithms into worksheet functions for solving virtually any computational problem that can be modelled by formulas and variables. Several examples are presented for computing integrals, derivatives, and systems of deferential-algebraic equations. Incorporation of the worksheet solver functions with the ubiquitous spreadsheet extend the utility of the latter as a powerful tool for computational mathematics.

Keywords: Calculus functions, nonlinear systems, differential algebraic equations, solvers, spreadsheet.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2402

Authors: Shai Sarussi

Abstract:

Let S be an integral domain with field of fractions F and let A be an F-algebra. An S-subalgebra R of A is called S-nice if R∩F = S and the localization of R with respect to S \{0} is A. Denoting by W the set of all S-nice subalgebras of A, and defining a notion of open sets on W, one can view W as a T0-Alexandroff space. Thus, the algebraic structure of W can be viewed from the point of view of topology. It is shown that every nonempty open subset of W has a maximal element in it, which is also a maximal element of W. Moreover, a supremum of an irreducible subset of W always exists. As a notable connection with valuation theory, one considers the case in which S is a valuation domain and A is an algebraic field extension of F; if S is indecomposed in A, then W is an irreducible topological space, and W contains a greatest element.

Keywords: Algebras over integral domains, Alexandroff topology, valuation domains, integral domains.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 448

Authors: Deepthi Haridas, S Venkataraman, Geeta Varadan

Abstract:

Quasigroups are algebraic structures closely related to Latin squares which have many different applications. The construction of block cipher is based on quasigroup string transformation. This article describes a block cipher based Quasigroup of order 256, suitable for fast software encryption of messages written down in universal ASCII code. The novelty of this cipher lies on the fact that every time the cipher is invoked a new set of two randomly generated quasigroups are used which in turn is used to create a pair of quasigroup of dual operations. The cryptographic strength of the block cipher is examined by calculation of the xor-distribution tables. In this approach some algebraic operations allows quasigroups of huge order to be used without any requisite to be stored.

Keywords: quasigroups, latin squares, block cipher and quasigroup string transformations.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2027

Authors: Noura Boudiaf, Allaoua Chaoui

Abstract:

One major difficulty that faces developers of concurrent and distributed software is analysis for concurrency based faults like deadlocks. Petri nets are used extensively in the verification of correctness of concurrent programs. ECATNets [2] are a category of algebraic Petri nets based on a sound combination of algebraic abstract types and high-level Petri nets. ECATNets have 'sound' and 'complete' semantics because of their integration in rewriting logic [12] and its programming language Maude [13]. Rewriting logic is considered as one of very powerful logics in terms of description, verification and programming of concurrent systems. We proposed in [4] a method for translating Ada-95 tasking programs to ECATNets formalism (Ada-ECATNet). In this paper, we show that ECATNets formalism provides a more compact translation for Ada programs compared to the other approaches based on simple Petri nets or Colored Petri nets (CPNs). Such translation doesn-t reduce only the size of program, but reduces also the number of program states. We show also, how this compact Ada-ECATNet may be reduced again by applying reduction rules on it. This double reduction of Ada-ECATNet permits a considerable minimization of the memory space and run time of corresponding Maude program.

Keywords: Ada tasking, ECATNets, Algebraic Petri Nets, Compact Representation, Analysis, Rewriting Logic, Maude.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1369

Authors: S. Banerjee

Abstract:

The paper describes design of an ontology in the financial domain for mutual funds. The design of this ontology consists of four steps, namely, specification, knowledge acquisition, implementation and semantic query. Specification includes a description of the taxonomy and different types mutual funds and their scope. Knowledge acquisition involves the information extraction from heterogeneous resources. Implementation describes the conceptualization and encoding of this data. Finally, semantic query permits complex queries to integrated data, mapping of these database entities to ontological concepts.

Keywords: Ontology, Semantic Web, Mutual Funds.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3602

Authors: Omid Sharifi, Member, ACM, Zeki Bayram, Member, ACM

Abstract:

We demonstrate through a sample application, Ebanking, that the Web Service Modelling Language Ontology component can be used as a very powerful object-oriented database design language with logic capabilities. Its conceptual syntax allows the definition of class hierarchies, and logic syntax allows the definition of constraints in the database. Relations, which are available for modelling relations of three or more concepts, can be connected to logical expressions, allowing the implicit specification of database content. Using a reasoning tool, logic queries can also be made against the database in simulation mode.

Keywords: Semantic web, ontology, E-banking, database, WSML, WSMO, E-R diagram.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1890

Authors: Rodrigo Chandia, Mauricio Papa

Abstract:

Efforts to secure supervisory control and data acquisition (SCADA) systems must be supported under the guidance of sound security policies and mechanisms to enforce them. Critical elements of the policy must be systematically translated into a format that can be used by policy enforcement components. Ideally, the goal is to ensure that the enforced policy is a close reflection of the specified policy. However, security controls commonly used to enforce policies in the IT environment were not designed to satisfy the specific needs of the SCADA environment. This paper presents a language, based on the well-known XACML framework, for the expression of authorization policies for SCADA systems.

Keywords: Access policy specification, process control systems, network security.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2246

Authors: Hassan Haghighi

Abstract:

Probabilistic techniques in computer programs are becoming more and more widely used. Therefore, there is a big interest in the formal specification, verification, and development of probabilistic programs. In our work-in-progress project, we are attempting to make a constructive framework for developing probabilistic programs formally. The main contribution of this paper is to introduce an intermediate artifact of our work, a Z-based formalism called PZ, by which one can build set theoretical models of probabilistic programs. We propose to use a constructive set theory, called CZ set theory, to interpret the specifications written in PZ. Since CZ has an interpretation in Martin-L¨of-s theory of types, this idea enables us to derive probabilistic programs from correctness proofs of their PZ specifications.

Keywords: formal specification, formal program development, probabilistic programs, CZ set theory, type theory.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1161

Authors: B. I. Yun

Abstract:

A dual-reciprocity boundary element method is presented for the numerical solution of a class of axisymmetric elastodynamic problems. The domain integrals that arise in the integrodifferential formulation are converted to line integrals by using the dual-reciprocity method together suitably constructed interpolating functions. The second order time derivatives of the displacement in the governing partial differential equations are suppressed by using Laplace transformation. In the Laplace transform domain, the problem under consideration is eventually reduced to solving a system of linear algebraic equations. Once the linear algebraic equations are solved, the displacement and stress fields in the physical domain can be recovered by using a numerical technique for inverting Laplace transforms.

Keywords: Axisymmetric elasticity, boundary element method, dual-reciprocity method, Laplace transform.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1620

Authors: Meemongkol A., Tipsuwanporn V., Numsomran A.

Abstract:

The authors present optimization parameters of rotary positioner controller in hard disk drive servo track writing process using coefficient diagram method; CDM. Due to estimation parameters in PI Positioning Control System by expected ratio method cannot meet the required specification of response effectively, we suggest coefficient diagram method for defining controller parameters under the requirement of the system. Finally, the simulation results show that our proposed method can improve the problem in tuning parameter of rotary positioner controller. It is satisfied specification of performance of control system. Furthermore, it is very convenient as a fast adjustment damping ratio as well as a high speed response.

Keywords: Optimization Parameters, Rotary Positioner, CDM

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1498

Authors: Petr Šimek, Kamil Kostruk

Abstract:

This paper deals with the problem of testing the Electronic Control Unit (ECU) for the specified function validation. Modern ECUs have many functions which need to be tested. This process requires tracking between the test and the specification. The technique discussed in this paper explores the system for automating this process. The paper focuses on the introduction to the problem in general, then it describes the proposed test system concept and its principle. It looks at how the process of the ECU interface specification file for automated interface testing and test tracking works. In the end, the future possible development of the project is discussed.

Keywords: Electronic control unit testing, embedded system, test generate, test automation, process automation, CAN bus, Ethernet.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 182

Authors: Samson Okwakol Ariko, Venansius Baryamureeba

Abstract:

Internet Access Technologies (IAT) provide a means through which Internet can be accessed. The choice of a suitable Internet technology is increasingly becoming an important issue to ISP clients. Currently, the choice of IAT is based on discretion and intuition of the concerned managers and the reliance on ISPs. In this paper we propose a model and designs algorithms that are used in the Internet access technology specification. In the proposed model, three ranking approaches are introduced; concurrent ranking, stepwise ranking and weighted ranking. The model ranks the IAT based on distance measures computed in ascending order while the global ranking system assigns weights to each IAT according to the position held in each ranking technique, determines the total weight of a particular IAT and ranks them in descending order. The final output is an objective ranking of IAT in descending order.

Keywords: Internet Access Technology (IAT).

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1395

Authors: Kamil Aida-zade, C. Ardil

Abstract:

In this paper, some problem formulations of dynamic object parameters recovery described by non-autonomous system of ordinary differential equations with multipoint unshared edge conditions are investigated. Depending on the number of additional conditions the problem is reduced to an algebraic equations system or to a problem of quadratic programming. With this purpose the paper offers a new scheme of the edge conditions transfer method called by conditions shift. The method permits to get rid from differential links and multipoint unshared initially-edge conditions. The advantage of the proposed approach is concluded by capabilities of reduction of a parametric identification problem to essential simple problems of the solution of an algebraic system or quadratic programming.

Keywords: dynamic objects, ordinary differential equations, multipoint unshared edge conditions, quadratic programming, conditions shift

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1424

Authors: Khair Eddin Sabri, Ridha Khedri, Jason Jaskolka

Abstract:

Cryptographic protocols are widely used in various applications to provide secure communications. They are usually represented as communicating agents that send and receive messages. These agents use their knowledge to exchange information and communicate with other agents involved in the protocol. An agent knowledge can be partitioned into explicit knowledge and procedural knowledge. The explicit knowledge refers to the set of information which is either proper to the agent or directly obtained from other agents through communication. The procedural knowledge relates to the set of mechanisms used to get new information from what is already available to the agent. In this paper, we propose a mathematical framework which specifies the explicit knowledge of an agent involved in a cryptographic protocol. Modelling this knowledge is crucial for the specification, analysis, and implementation of cryptographic protocols. We also, report on a prototype tool that allows the representation and the manipulation of the explicit knowledge.

Keywords: Information Algebra, Agent Knowledge, CryptographicProtocols

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1426

Authors: Cencen Li, Shaoying Liu, Shin Nakajima

Abstract:

Specification-based testing enables us to detect errors in the implementation of functions defined in given specifications. Its effectiveness in achieving high path coverage and efficiency in generating test cases are always major concerns of testers. The automatic test cases generation approach based on formal specifications proposed by Liu and Nakajima is aimed at ensuring high effectiveness and efficiency, but this approach has not been empirically assessed. In this paper, we present an experiment for assessing Liu-s testing approach. The result indicates that this testing approach may not be effective in some circumstances. We discuss the result, analyse the specific causes for the ineffectiveness, and describe some suggestions for improvement.

Keywords: experiment, functional scenario, specification-based, testing.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1661

Authors: Pongchanun Luangpaiboon, Wanwisa Sarasang

Abstract:

In this paper, performances of shuffled frog leaping algorithm was investigated on the stealth laser dicing process. Effect of problem on the performance of the algorithm was based on the tolerance of meandering data. From the customer specification it could be less than five microns with the target of zero microns. Currently, the meandering levels are unsatisfactory when compared to the customer specification. Firstly, the two-level factorial design was applied to preliminarily study the statistically significant effects of five process variables. In this study one influential process variable is integer. From the experimental results, the new operating condition from the algorithm was superior when compared to the current manufacturing condition.

Keywords: Stealth Laser Dicing Process, Meandering, Metaheuristics, Shuffled Frog Leaping Algorithm.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2586

Authors: Alexander N. Savostyanov, Tatiana A. Dolgorukova, Elena A. Esipenko, Mikhail S. Zaleshin, Margherita Malanchini, Anna V. Budakova, Alexander E. Saprygin, Tatiana A. Golovko, Yulia V. Kovas

Abstract:

EEG correlates of mathematical and trait anxiety level were studied in 52 healthy Russian-speakers during execution of error-recognition tasks with lexical, arithmetic and algebraic conditions. Event-related spectral perturbations were used as a measure of brain activity. The ERSP plots revealed alpha/beta desynchronizations within a 500-3000 ms interval after task onset and slow-wave synchronization within an interval of 150-350 ms. Amplitudes of these intervals reflected the accuracy of error recognition, and were differently associated with the three conditions. The correlates of anxiety were found in theta (4-8 Hz) and beta2 (16- 20 Hz) frequency bands. In theta band the effects of mathematical anxiety were stronger expressed in lexical, than in arithmetic and algebraic condition. The mathematical anxiety effects in theta band were associated with differences between anterior and posterior cortical areas, whereas the effects of trait anxiety were associated with inter-hemispherical differences. In beta1 and beta2 bands effects of trait and mathematical anxiety were directed oppositely. The trait anxiety was associated with increase of amplitude of desynchronization, whereas the mathematical anxiety was associated with decrease of this amplitude. The effect of mathematical anxiety in beta2 band was insignificant for lexical condition but was the strongest in algebraic condition. EEG correlates of anxiety in theta band could be interpreted as indexes of task emotionality, whereas the reaction in beta2 band is related to tension of intellectual resources.

Keywords: EEG, brain activity, lexical and numerical error-recognition tasks, mathematical and trait anxiety.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1887

Authors: Yanchao Wang, Rajshekhar Sunderraman

Abstract:

This paper presents an algebraic approach to optimize queries in domain-specific database management system for protein structure data. The approach involves the introduction of several protein structure specific algebraic operators to query the complex data stored in an object-oriented database system. The Protein Algebra provides an extensible set of high-level Genomic Data Types and Protein Data Types along with a comprehensive collection of appropriate genomic and protein functions. The paper also presents a query translator that converts high-level query specifications in algebra into low-level query specifications in Protein-QL, a query language designed to query protein structure data. The query transformation process uses a Protein Ontology that serves the purpose of a dictionary.

Keywords: Domain-Specific Data Management, Protein Algebra, Protein Ontology, Protein Structure Data.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1491

Authors: Noura Boudiaf, Abdelhamid Djebbar

Abstract:

Colored Petri Nets (CPN) are very known kind of high level Petri nets. With sound and complete semantics, rewriting logic is one of very powerful logics in description and verification of non-deterministic concurrent systems. Recently, CPN semantics are defined in terms of rewriting logic, allowing us to built models by formal reasoning. In this paper, we propose an automatic translation of CPN to the rewriting logic language Maude. This tool allows graphical editing and simulating CPN. The tool allows the user drawing a CPN graphically and automatic translating the graphical representation of the drawn CPN to Maude specification. Then, Maude language is used to perform the simulation of the resulted Maude specification. It is the first rewriting logic based environment for this category of Petri Nets.

Keywords: Colored Petri Nets, Rewriting Logic, Maude, Graphical Edition, Automatic Translation, Simulation.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1560

Authors: Saleh A. Al-Jufout

Abstract:

This paper presents a procedure of forming the mathematical model of radial electric power systems for simulation of both transient and steady-state conditions. The research idea has been based on nodal voltages technique and on differentiation of Kirchhoff's current law (KCL) applied to each non-reference node of the radial system, the result of which the nodal voltages has been calculated by solving a system of algebraic equations. Currents of the electric power system components have been determined by solving their respective differential equations. Transforming the three-phase coordinate system into Cartesian coordinate system in the model decreased the overall number of equations by one third. The use of Cartesian coordinate system does not ignore the DC component during transient conditions, but restricts the model's implementation for symmetrical modes of operation only. An example of the input data for a four-bus radial electric power system has been calculated.

Keywords: Mathematical Modelling, Radial Power System, Steady-State, Transients

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1215

Authors: Md. Alal Hosen

Abstract:

In this paper, a modified harmonic balance method based an analytical technique has been developed to determine higher-order approximate periodic solutions of a conservative nonlinear oscillator for which the elastic force term is proportional to x^1/3. Usually, a set of nonlinear algebraic equations is solved in this method. However, analytical solutions of these algebraic equations are not always possible, especially in the case of a large oscillation. In this article, different parameters of the same nonlinear problems are found, for which the power series produces desired results even for the large oscillation. We find a modified harmonic balance method works very well for the whole range of initial amplitudes, and the excellent agreement of the approximate frequencies and periodic solutions with the exact ones has been demonstrated and discussed. Besides these, a suitable truncation formula is found in which the solution measures better results than existing solutions. The method is mainly illustrated by the x^1/3 force nonlinear oscillator but it is also useful for many other nonlinear problems.

Keywords: Approximate solutions, Harmonic balance method, Nonlinear oscillator, Perturbation.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1383

Authors: Linda, Sau-ling Lai

Abstract:

This paper provides new ways to explore the old problem of failure of information systems development in an organisation. Based on the theory of cognitive dissonance, information systems (IS) failure is defined as a gap between what the users expect from an information system and how well these expectations are met by the perceived performance of the delivered system. Bridging the expectation-perception gap requires that IS professionals make a radical change from being the proprietor of information systems and products to being service providers. In order to deliver systems and services that IS users perceive as valuable, IS people must become expert in determining and assessing users- expectations and perceptions. It is also suggested that the IS community, in general, has given relatively little attention to the front-end process of requirements specification for IS development. There is a simplistic belief that requirements are obtainable from users, they are then translatable into a formal specification. The process of information needs analysis is problematic and worthy of investigation.

Keywords: Information Systems Development, Cognitive Dissonance, Expectation-Perception Gap, Requirements Analysis.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3600

Authors: Nazir Ahmad Zafar, Nabeel Sabir, Amir Ali

Abstract:

Functionalities and control behavior are both primary requirements in design of a complex system. Automata theory plays an important role in modeling behavior of a system. Z is an ideal notation which is used for describing state space of a system and then defining operations over it. Consequently, an integration of automata and Z will be an effective tool for increasing modeling power for a complex system. Further, nondeterministic finite automata (NFA) may have different implementations and therefore it is needed to verify the transformation from diagrams to a code. If we describe formal specification of an NFA before implementing it, then confidence over transformation can be increased. In this paper, we have given a procedure for integrating NFA and Z. Complement of a special type of NFA is defined. Then union of two NFAs is formalized after defining their complements. Finally, formal construction of intersection of NFAs is described. The specification of this relationship is analyzed and validated using Z/EVES tool.

Keywords: Modeling, Nondeterministic finite automata, Znotation, Integration of approaches, Validation.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3137

Authors: Wei Hoo Chong

Abstract:

System testing is actually done to the entire system against the Functional Requirement Specification and/or the System Requirement Specification. Moreover, it is an investigatory testing phase, where the focus is to have almost a destructive attitude and test not only the design, but also the behavior and even the believed expectations of the customer. It is also intended to test up to and beyond the bounds defined in the software/hardware requirements specifications. In Motorola®, Automated Testing is one of the testing methodologies uses by GSG-iSGT (Global Software Group - iDEN TM Subcriber Group-Test) to increase the testing volume, productivity and reduce test cycle-time in iDEN TM phones testing. Testing is able to produce more robust products before release to the market. In this paper, iHopper is proposed as a tool to perform stress test on iDEN TM phonse. We will discuss the value that automation has brought to iDEN TM Phone testing such as improving software quality in the iDEN TM phone together with some metrics. We will also look into the advantages of the proposed system and some discussion of the future work as well.

Keywords: Testing, automated testing, stress testing, software quality.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1444

Authors: Morteza Talebi, Jianan Wang, Zhihua Qu

Abstract:

The security of power systems against malicious cyberphysical data attacks becomes an important issue. The adversary always attempts to manipulate the information structure of the power system and inject malicious data to deviate state variables while evading the existing detection techniques based on residual test. The solutions proposed in the literature are capable of immunizing the power system against false data injection but they might be too costly and physically not practical in the expansive distribution network. To this end, we define an algebraic condition for trustworthy power system to evade malicious data injection. The proposed protection scheme secures the power system by deterministically reconfiguring the information structure and corresponding residual test. More importantly, it does not require any physical effort in either microgrid or network level. The identification scheme of finding meters being attacked is proposed as well. Eventually, a well-known IEEE 30-bus system is adopted to demonstrate the effectiveness of the proposed schemes.

Keywords: Algebraic Criterion, Malicious Cyber-Physical Data Injection, Protection and Identification, Trustworthy Power System.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1949

Authors: YongXian, JIN

Abstract:

Introducing survivability into embedded real-time system (ERTS) can improve the survivability power of the system. This paper mainly discusses about the survivability of ERTS. The first is the survivability origin of ERTS. The second is survivability analysis. According to the definition of survivability based on survivability specification and division of the entire survivability analysis process for ERTS, a survivability analysis profile is presented. The quantitative analysis model of this profile is emphasized and illuminated in detail, the quantifying analysis of system was showed helpful to evaluate system survivability more accurate. The third is platform design of survivability analysis. In terms of the profile, the analysis process is encapsulated and assembled into one platform, on which quantification, standardization and simplification of survivability analysis are all achieved. The fourth is survivability design. According to character of ERTS, strengthened design method is selected to realize system survivability design. Through the analysis of embedded mobile video-on-demand system, intrusion tolerant technology is introduced in whole survivability design.

Keywords: ERTS (embedded real-time system), survivability, quantitative analysis, survivability specification, intrusion tolerant

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1263

Authors: Zainab M. Musa, Nordin M. A. Rahman, Julaily A. Jusoh

Abstract:

Digital reference service is when a traditional library reference service is provided electronically. In most cases users do not get full satisfaction from using digital reference service due to variety of reasons. This paper discusses the formal specification of web services applications for digital reference services (WSDRS). WSDRS is an informal model that claims to reduce the problems of digital reference services in libraries. It uses web services technology to provide efficient digital way of satisfying users’ need in the reference section of libraries. Informal model is in natural language which is inconsistent and ambiguous that may cause difficulties to the developers of the system. In order to solve this problem we decided to convert the informal specifications into formal specifications. This is supposed to reduce the overall development time and cost. We use Z language to develop the formal model and verify it with Z/EVES theorem prover tool.

Keywords: Formal, specifications, web services, digital reference services.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1571

Authors: N. Boudiaf

Abstract:

One major difficulty that faces developers of concurrent and distributed software is analysis for concurrency based faults like deadlocks. Petri nets are used extensively in the verification of correctness of concurrent programs. ECATNets are a category of algebraic Petri nets based on a sound combination of algebraic abstract types and high-level Petri nets. ECATNets have 'sound' and 'complete' semantics because of their integration in rewriting logic and its programming language Maude. Rewriting logic is considered as one of very powerful logics in terms of description, verification and programming of concurrent systems We proposed previously a method for translating Ada-95 tasking programs to ECATNets formalism (Ada-ECATNet) and we showed that ECATNets formalism provides a more compact translation for Ada programs compared to the other approaches based on simple Petri nets or Colored Petri nets. We showed also previously how the ECATNet formalism offers to Ada many validation and verification tools like simulation, Model Checking, accessibility analysis and static analysis. In this paper, we describe the implementation of our translation of the Ada programs into ECATNets.

Keywords: Ada tasking, Analysis, Automatic Translation, ECATNets, Maude, Rewriting Logic.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1549

Authors: Nhon Do, Hien Nguyen

Abstract:

Nowadays there are many methods for representing knowledge such as semantic network, neural network, and conceptual graphs. Nonetheless, these methods are not sufficiently efficient when applied to perform and deduce on knowledge domains about supporting in general education such as algebra, analysis or plane geometry. This leads to the introduction of computational network which is a useful tool for representation knowledge base, especially for computational knowledge, especially knowledge domain about general education. However, when dealing with a practical problem, we often do not immediately find a new solution, but we search related problems which have been solved before and then proposing an appropriate solution for the problem. Besides that, when finding related problems, we have to determine whether the result of them can be used to solve the practical problem or not. In this paper, the extension model of computational network has been presented. In this model, Sample Problems, which are related problems, will be used like the experience of human about practical problem, simulate the way of human thinking, and give the good solution for the practical problem faster and more effectively. This extension model is applied to construct an automatic system for solving algebraic problems in middle school.

Keywords: educational software, artificial intelligence, knowledge base system, knowledge representation.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1634