Search results for: Formal proof system

Authors: Sebastian Kusch, Markus Kaiser

Abstract:

In this paper we analyze the application of a formal proof system to the discrete logarithm problem used in publickey cryptography. That means, we explore a computer verification of the ElGamal encryption scheme with the formal proof system Isabelle/HOL. More precisely, the functional correctness of this algorithm is formally verified with computer support. Besides, we present a formalization of the DSA signature scheme in the Isabelle/HOL system. We show that this scheme is correct what is a necessary condition for the usefulness of any cryptographic signature scheme.

Keywords: Formal proof system, higher-order logic, formal verification, cryptographic signature scheme.

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

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this article we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (σ-algebras, probability spaces and conditional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes- Formula. Besides, we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this article shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in cryptographic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) probabilitydistributions, formal proof system, higher-order logic, formalverification, Bayes' Formula, Miller-Rabin primality test.

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

Authors: Johannes Buchmann, Markus Kaiser

Abstract:

We decribe a formal specification and verification of the Rabin public-key scheme in the formal proof system Is-abelle/HOL. The idea is to use the two views of cryptographic verification: the computational approach relying on the vocabulary of probability theory and complexity theory and the formal approach based on ideas and techniques from logic and programming languages. The analysis presented uses a given database to prove formal properties of our implemented functions with computer support. Thema in task in designing a practical formalization of correctness as well as security properties is to cope with the complexity of cryptographic proving. We reduce this complexity by exploring a light-weight formalization that enables both appropriate formal definitions as well as eficient formal proofs. This yields the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Consequently, we get reliable proofs with a minimal error rate augmenting the used database. This provides a formal basis for more computer proof constructions in this area.

Keywords: public-key encryption, Rabin public-key scheme, formalproof system, higher-order logic, formal verification.

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

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this paper we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (o--algebras, probability spaces and condi¬tional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes' Formula. Besides we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this paper shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in crypto-graphic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) proba¬bility distributions, formal proof system, higher-order logic, formal verification, Bayes' Formula, Miller-Rabin primality test.

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

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this article, a formal specification and verification of the Rabin public-key scheme in a formal proof system is presented. The idea is to use the two views of cryptographic verification: the computational approach relying on the vocabulary of probability theory and complexity theory and the formal approach based on ideas and techniques from logic and programming languages. A major objective of this article is the presentation of the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Moreover, we explicate a (computer-proven) formalization of correctness as well as a computer verification of security properties using a straight-forward computation model in Isabelle/HOL. The analysis uses a given database to prove formal properties of our implemented functions with computer support. The main task in designing a practical formalization of correctness as well as efficient computer proofs of security properties is to cope with the complexity of cryptographic proving. We reduce this complexity by exploring a light-weight formalization that enables both appropriate formal definitions as well as efficient formal proofs. Consequently, we get reliable proofs with a minimal error rate augmenting the used database, what provides a formal basis for more computer proof constructions in this area.

Keywords: public-key encryption, Rabin public-key scheme, formalproof system, higher-order logic, formal verification.

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

Authors: Eric Filiol

Abstract:

This paper presents a formalisation of the different existing code mutation techniques (polymorphism and metamorphism) by means of formal grammars. While very few theoretical results are known about the detection complexity of viral mutation techniques, we exhaustively address this critical issue by considering the Chomsky classification of formal grammars. This enables us to determine which family of code mutation techniques are likely to be detected or on the contrary are bound to remain undetected. As an illustration we then present, on a formal basis, a proof-of-concept metamorphic mutation engine denoted PB MOT, whose detection has been proven to be undecidable.

Keywords: Polymorphism, Metamorphism, Formal Grammars, Formal Languages, Language Decision, Code Mutation, Word Problem

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

Authors: HyoungMin Ham, JooSeok Song

Abstract:

RFID tag is a small and inexpensive microchip which is capable of transmitting unique identifier through wireless network in a short distance. If a group of RFID tags can be scanned simultaneously by one reader, RFID Group proof could be generated. Group proof can be used in various applications, such as good management which is usually achieved using barcode system. A lot of RFID group proof schemes have been proposed by many researchers. In this paper, we introduce some existing group proof schemes and then analyze their vulnerabilities to the privacy. Moreover, we propose a new attack model, which threats the privacy of user by tracking tags in a group.

Keywords: grouping proof, privacy, RFID, yoking proof

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

Authors: Guowei Hou, Lixin Yu, Wei Zhuang, Hui Qin, Xue Yang

Abstract:

Formal verification is proposed to ensure the correctness of the design and make functional verification more efficient. As cache plays a vital role in the design of System on Chip (SoC), and cache with Memory Management Unit (MMU) and cache memory unit makes the state space too large for simulation to verify, then a formal verification is presented for such system design. In the paper, a formal model checking verification flow is suggested and a new cache memory model which is called “exhaustive search model” is proposed. Instead of using large size ram to denote the whole cache memory, exhaustive search model employs just two cache blocks. For cache system contains data cache (Dcache) and instruction cache (Icache), Dcache memory model and Icache memory model are established separately using the same mechanism. At last, the novel model is employed to the verification of a cache which is module of a custom-built SoC system that has been applied in practical, and the result shows that the cache system is verified correctly using the exhaustive search model, and it makes the verification much more manageable and flexible.

Keywords: Cache system, formal verification, novel model, System on Chip (SoC).

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

Authors: Mubina Nazmeen, Iram Rubab

Abstract:

Formal Specification languages are being widely used for system specification and testing. Highly critical systems such as real time systems, avionics, and medical systems are represented using Formal specification languages. Formal specifications based testing is mostly performed using black box testing approaches thus testing only the set of inputs and outputs of the system. The formal specification language such as VDMµ can be used for white box testing as they provide enough constructs as any other high level programming language. In this work, we perform data and control flow analysis of VDMµ class specifications. The proposed work is discussed with an example of SavingAccount.

Keywords: VDM-SL, VDMµ, data flow graph, control flowgraph, testing, formal specification.

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

Authors: Kazuo Komatsu, Hitoshi Takata

Abstract:

The objective of this study is to propose an observer design for nonlinear systems by using an augmented linear system derived by application of a formal linearization method. A given nonlinear differential equation is linearized by the formal linearization method which is based on Taylor expansion considering up to the higher order terms, and a measurement equation is transformed into an augmented linear one. To this augmented dimensional linear system, a linear estimation theory is applied and a nonlinear observer is derived. As an application of this method, an estimation problem of transient state of electric power systems is studied, and its numerical experiments indicate that this observer design shows remarkable performances for nonlinear systems.

Keywords: nonlinear system, augmented linear system, nonlinear observer, formal linearization, electric power system.

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

Authors: Kazuo Komatsu, Hitoshi Takata

Abstract:

This paper discusses a design of nonlinear observer by a formal linearization method using an application of Chebyshev Interpolation in order to facilitate processes for synthesizing a nonlinear observer and to improve the precision of linearization. A dynamic nonlinear system is linearized with respect to a linearization function, and a measurement equation is transformed into an augmented linear one by the formal linearization method which is based on Chebyshev interpolation. To the linearized system, a linear estimation theory is applied and a nonlinear observer is derived. To show effectiveness of the observer design, numerical experiments are illustrated and they indicate that the design shows remarkable performances for nonlinear systems.

Keywords: nonlinear system, nonlinear observer, formal linearization, Chebyshev interpolation.

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

Authors: Rajaa Filali, Mohamed Bouhdadi

Abstract:

This paper presents an incremental formal development of the Wireless Transaction Protocol (WTP) in Event-B. WTP is part of the Wireless Application Protocol (WAP) architectures and provides a reliable request-response service. To model and verify the protocol, we use the formal technique Event-B which provides an accessible and rigorous development method. This interaction between modelling and proving reduces the complexity and helps to eliminate misunderstandings, inconsistencies, and specification gaps. As result, verification of WTP allows us to find some deficiencies in the current specification.

Keywords: Event-B, wireless transaction protocol, refinement, proof obligation, Rodin, ProB.

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

Authors: Kei Kawamorita, Ryouta Kasahara, Yuuki Mochizuki, Kenichiro Noguchi

Abstract:

A separation-kernel-based operating system (OS) has been designed for use in secure embedded systems by applying formal methods to the design of the separation-kernel part. The separation kernel is a small OS kernel that provides an abstract distributed environment on a single CPU. The design of the separation kernel was verified using two formal methods, the B method and the Spin model checker. A newly designed semi-formal method, the extended state transition method, was also applied. An OS comprising the separation-kernel part and additional OS services on top of the separation kernel was prototyped on the Intel IA-32 architecture. Developing and testing of a prototype embedded application, a point-of-sale application, on the prototype OS demonstrated that the proposed architecture and the use of formal methods to design its kernel part are effective for achieving a secure embedded system having a high-assurance separation kernel.

Keywords: B method, embedded systems, extended state transition, formal methods, separation kernel, Spin.

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

Authors: Mohamed A. Sullabi

Abstract:

The importance of the formal specification in the software life cycle is barely concealing to anyone. Formal specifications use mathematical notation to describe the properties of information system precisely, without unduly constraining the way in how these properties are achieved. Having a correct and quality software specification is not easy task. This study concerns with how a group of rectifiers can communicate with each other and work to prepare and produce a correct formal software specification. WBCS has been implemented based mainly in the proposed supported cooperative work model and a survey conducted on the existing Webbased collaborative writing tools. This paper aims to assess the feasibility of executing the web-based collaboration process using WBCS. The purpose of conducting this test is to test the system as a whole for functionality and fitness for use based on the evaluation test plan.

Keywords: Formal methods, Formal specifications, collaborative writing, Usability testing.

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

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 1615

Authors: Kazuo Komatsu, Hitoshi Takata

Abstract:

In this paper we consider a nonlinear control design for nonlinear systems by using two-stage formal linearization and twotype LQ controls. The ordinary LQ control is designed on almost linear region around the steady state point. On the other region, another control is derived as follows. This derivation is based on coordinate transformation twice with respect to linearization functions which are defined by polynomials. The linearized systems can be made up by using Taylor expansion considered up to the higher order. To the resulting formal linear system, the LQ control theory is applied to obtain another LQ control. Finally these two-type LQ controls are smoothly united to form a single nonlinear control. Numerical experiments indicate that this control show remarkable performances for a nonlinear system.

Keywords: Formal Linearization, LQ Control, Nonlinear Control, Taylor Expansion, Zero Function.

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

Authors: Gilbert Ndjatou

Abstract:

We propose a formal framework for the specification of the behavior of a system of agents, as well as those of the constituting agents. This framework allows us to model each agent-s effectoric capability including its interactions with the other agents. We also provide an algorithm based on Milner-s "observation equivalence" to derive an agent-s perception of its task domain situations from its effectoric capability, and use "system computations" to model the coordinated efforts of the agents in the system . Formal definitions of the concept of "behavior equivalence" of two agents and that of system computations equivalence for an agent are also provided.

Keywords: Multiagent system, object system, observation equivalence, reactive systems.

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

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

Abstract:

The web services applications for digital reference service (WSDRS) of LIS model is an informal model that claims to reduce the problems of digital reference services in libraries. It uses web services technology to provide efficient way of satisfying users’ needs in the reference section of libraries. The formal WSDRS model consists of the Z specifications of all the informal specifications of the model. This paper discusses the formal validation of the Z specifications of WSDRS model. The authors formally verify and thus validate the properties of the model using Z/EVES theorem prover.

Keywords: Validation, verification, formal, theorem proving.

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

Authors: Abdelaziz Guerrouat, Harald Richter

Abstract:

In this paper test generation methods and appropriate fault models for testing and analysis of embedded systems described as (extended) finite state machines ((E)FSMs) are presented. Compared to simple FSMs, EFSMs specify not only the control flow but also the data flow. Thus, we define a two-level fault model to cover both aspects. The goal of this paper is to reuse well-known FSM-based test generation methods for automation of embedded system testing. These methods have been widely used in testing and validation of protocols and communicating systems. In particular, (E)FSMs-based specification and testing is more advantageous because (E)FSMs support the formal semantic of already standardised formal description techniques (FDTs) despite of their popularity in the design of hardware and software systems.

Keywords: Formal methods, testing and validation, finite state machines, formal description techniques.

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

Authors: Sara Sharifi Rad, Hassan Haghighi

Abstract:

Due to important issues, such as deadlock, starvation, communication, non-deterministic behavior and synchronization, concurrent systems are very complex, sensitive, and error-prone. Thus ensuring reliability and accuracy of these systems is very essential. Therefore, there has been a big interest in the formal specification of concurrent programs in recent years. Nevertheless, some features of concurrent systems, such as dynamic process creation, scheduling and starvation have not been specified formally yet. Also, some other features have been specified partially and/or have been described using a combination of several different formalisms and methods whose integration needs too much effort. In other words, a comprehensive and integrated specification that could cover all aspects of concurrent systems has not been provided yet. Thus, this paper makes two major contributions: firstly, it provides a comprehensive formal framework to specify all well-known features of concurrent systems. Secondly, it provides an integrated specification of these features by using just a single formal notation, i.e., the Z language.

Keywords: Concurrent systems, Formal methods, Formal specification, Z language

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

Authors: Eric Filiol

Abstract:

This paper presents a protocol aiming at proving that an encryption system contains structural weaknesses without disclosing any information on those weaknesses. A verifier can check in a polynomial time that a given property of the cipher system output has been effectively realized. This property has been chosen by the prover in such a way that it cannot been achieved by known attacks or exhaustive search but only if the prover indeed knows some undisclosed weaknesses that may effectively endanger the cryptosystem security. This protocol has been denoted zero-knowledge-like proof of cryptanalysis. In this paper, we apply this protocol to the Bluetooth core encryption algorithm E0, used in many mobile environments and thus we suggest that its security can seriously be put into question.

Keywords: Bluetooth encryption, Bluetooth security, Bluetoothprotocol, Stream cipher, Zero-knowledge, Cryptanalysis

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

Authors: Basyir Yaman, Fades Br. Gultom

Abstract:

The picture and pattern of Islamic education in the Prophet's period in Mecca and Medina is the history of the past that we need to bring back. The Basic Education Institute called Kuttab. Kuttab or Maktab comes from the word kataba which means to write. The popular Kuttab in the Prophet’s period aims to resolve the illiteracy in the Arab community. In Indonesia, this Institution has 25 branches; one of them is located in Semarang (i.e. Kuttab Al-Fatih). Kuttab Al-Fatih as a non-formal institution of Islamic education is reserved for children aged 5-12 years. The independently designed curriculum is a distinctive feature that distinguishes between Kuttab Al-Fatih curriculum and the formal institutional curriculum in Indonesia. The curriculum includes the faith and the Qur’an. Kuttab Al-Fatih has been licensed as a Community Activity Learning Center under the direct supervision and guidance of the National Education Department. Here, we focus to describe the implementation of curriculum Kuttab Al-Fatih Semarang (i.e. faith and al-Qur’an). After that, we determine the relevance between the implementation of the Kuttab Al-Fatih education system with the formal education system in Indonesia. This research uses literature review and field research qualitative methods. We obtained the data from the head of Kuttab Al-Fatih Semarang, vice curriculum, faith coordinator, al-Qur’an coordinator, as well as the guardians of learners and the learners. The result of this research is the relevance of education system in Kuttab Al-Fatih Semarang about education system in Indonesia. Kuttab Al-Fatih Semarang emphasizes character building through a curriculum designed in such a way and combines thematic learning models in modules.

Keywords: Islamic education system, implementation of curriculum, Kuttab Al-Fatih semarang, formal education system in Indonesia.

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

Authors: Wiem Gadri

Abstract:

This study delves into the intriguing properties of Pisot and Salem numbers within the framework of formal Laurent series over finite fields, a domain where these numbers’ spectral characteristics, Λm(β) and lm(β), have yet to be fully explored. Utilizing a methodological approach that combines algebraic number theory with the analysis of power series, we extend the foundational work of Erdos, Joo, and Komornik to this setting. Our research uncovers bounds for lm(β), revealing how these depend on the degree of the minimal polynomial of β and thus offering a characterization of Pisot and Salem formal power series. The findings significantly contribute to our understanding of these numbers, highlighting their distribution and properties in the context of formal power series. This investigation not only bridges number theory with formal power series analysis but also sets the stage for further interdisciplinary research in these areas.

Keywords: Pisot numbers, Salem numbers, Formal power series, Minimal polynomial degree.

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

Authors: Chanoknart Mayusoh

Abstract:

The research about Formal Thai National Costume in the reign of King Bhumibol Adulyadej is an applied research that aimed to study the accurate knowledge concerning to Thai national costume in the reign of King Rama IX, also to study origin of all costumes in the reign of King Rama IX and to study the style, material used, and using accasion. This research methodology which are collect quanlitative data through observation, document, and photograph from key informant of costume in the reign of King Rama IX and from another who related to this field.

The formal Thai national costume of the reign of King Bhumibol Adulyadej originated from the visit of His Majesty the King to Europe and America in 1960. Since Thailand had no traditional national costume; Her Majesty the Queen initiated the idea to create formal Thai national costumes. In 1964, Her Majesty the Queen selected 8 styles of formal Thai national costume. Later, Her Majesty the Queen confered another 3 formal Thai national costume for men. There are 8 styles of formal Thai national costume for women: Thai Ruean Ton, Thai Chit Lada, Thai Amarin, Thai Borom Phiman, Thai Siwalia, Thai Chakkri, Thai Dusit, and Thai Chakkraphat. There are 3 styles of formal Thai national costume for men: short-sleeve shirt, long-sleeve shirt, and long-sleeve shirt with breechcloth. The costume is widely used in formal ceremony such as greeting ceremony for official foreign visitors, wedding ceremony, or other auspicious ceremonies. Now a day, they are always used as a bridal gown as well. The formal Thai national costume is valuable art that shows Thai identity and, should be preserved for the next generation.

Keywords: The formal Thai national costume for women, The formal Thai national costume for men, His Majesty King Bhumibol Adulyadej the Great King Rama IX, Her Majesty Queen Sirikit Queen.

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

Authors: Frode van der Laak

Abstract:

The paper contributes to the feasibility of using a 5G mobile connection as a node for a Proof of Authority (PoA) blockchain, which is used for microtransactions at the same time. It uses the phone number identity of the users that are linked to the crypto wallet address. It also proposed a consensus protocol based on PoA blockchain; PoA is a permission blockchain where consensus is achieved through a set of designated authority rather than through mining, as is the case with a Proof of Work (PoW) blockchain. This report will first explain the concept of a PoA blockchain and how it works. It will then discuss the potential benefits and challenges of using a 5G mobile connection as a node in such a blockchain, and finally, the main open problem statement and proposed solutions with the requirements.

Keywords: 5G, mobile, connection, node, PoA, blockchain, microtransaction.

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

Authors: Amol A. Talankar, Prakash Verma, Nitin Seth

Abstract:

The purpose of this study is to identify the critical success factors (CSFs) for the effective implementation of Six Sigma in non-formal service Sectors.

Based on the survey of literature, the critical success factors (CSFs) for Six Sigma have been identified and are assessed for their importance in Non-formal service sector using Delphi Technique. These selected CSFs were put forth to the panel of expert to cluster them and prepare cognitive map to establish their relationship.

All the critical success factors examined and obtained from the review of literature have been assessed for their importance with respect to their contribution to Six Sigma effectiveness in non formal service sector.

The study is limited to the non-formal service sectors involved in the organization of religious festival only. However, the similar exercise can be conducted for broader sample of other non-formal service sectors like temple/ashram management, religious tours management etc.

The research suggests an approach to identify CSFs of Six Sigma for Non-formal service sector. All the CSFs of the formal service sector will not be applicable to Non-formal services, hence opinion of experts was sought to add or delete the CSFs. In the first round of Delphi, the panel of experts has suggested, two new CSFs-“competitive benchmarking (F19) and resident’s involvement (F28)”, which were added for assessment in the next round of Delphi.  One of the CSFs-“fulltime six sigma personnel (F15)” has been omitted in proposed clusters of CSFs for non-formal organization, as it is practically impossible to deploy full time trained Six Sigma recruits.

Keywords: Critical success factors (CSFs), Quality assurance, non-formal service sectors, Six Sigma.

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

Authors: George Eleftherakis, Petros Kefalas, Anna Sotiriadou, Evangelos Kehris

Abstract:

Recent advances in both the testing and verification of software based on formal specifications of the system to be built have reached a point where the ideas can be applied in a powerful way in the design of agent-based systems. The software engineering research has highlighted a number of important issues: the importance of the type of modeling technique used; the careful design of the model to enable powerful testing techniques to be used; the automated verification of the behavioural properties of the system; the need to provide a mechanism for translating the formal models into executable software in a simple and transparent way. This paper introduces the use of the X-machine formalism as a tool for modeling biology inspired agents proposing the use of the techniques built around X-machine models for the construction of effective, and reliable agent-based software systems.

Keywords: Biology inspired agent, formal methods, x-machines.

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

Authors: Anamika Gupta, Naveen Kumar, Vasudha Bhatnagar

Abstract:

This paper focuses on analyzing medical diagnostic data using classification rules in data mining and context reduction in formal concept analysis. It helps in finding redundancies among the various medical examination tests used in diagnosis of a disease. Classification rules have been derived from positive and negative association rules using the Concept lattice structure of the Formal Concept Analysis. Context reduction technique given in Formal Concept Analysis along with classification rules has been used to find redundancies among the various medical examination tests. Also it finds out whether expensive medical tests can be replaced by some cheaper tests.

Keywords: Data Mining, Formal Concept Analysis, Medical Data, Negative Classification Rules.

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

Authors: Yun Bai

Abstract:

This paper is to investigate the impplementation of security mechanism in object oriented database system. Formal methods plays an essential role in computer security due to its powerful expressiveness and concise syntax and semantics. In this paper, both issues of specification and implementation in database security environment will be considered; and the database security is achieved through the development of an efficient implementation of the specification without compromising its originality and expressiveness.

Keywords: database security, authorization policy, logic basedspecification

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

Authors: Rozilawati Razali, Paul W. Garratt

Abstract:

Software maintenance, which involves making enhancements, modifications and corrections to existing software systems, consumes more than half of developer time. Specification comprehensibility plays an important role in software maintenance as it permits the understanding of the system properties more easily and quickly. The use of formal notation such as B increases a specification-s precision and consistency. However, the notation is regarded as being difficult to comprehend. Semi-formal notation such as the Unified Modelling Language (UML) is perceived as more accessible but it lacks formality. Perhaps by combining both notations could produce a specification that is not only accurate and consistent but also accessible to users. This paper presents an experiment conducted on a model that integrates the use of both UML and B notations, namely UML-B, versus a B model alone. The objective of the experiment was to evaluate the comprehensibility of a UML-B model compared to a traditional B model. The measurement used in the experiment focused on the efficiency in performing the comprehension tasks. The experiment employed a cross-over design and was conducted on forty-one subjects, including undergraduate and masters students. The results show that the notation used in the UML-B model is more comprehensible than the B model.

Keywords: Model comprehensibility, formal and semi-formal notation, empirical assessment.

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