Search

In remote villages without access to modern IT technology, simple devices such as smartcards can be used to carry out business transactions. These devices typically store multiple business applications from multiple vendors. Although devices must prevent malicious or accidental security breaches among the applications, a secure communication channel between two applications from different vendors is often required. In this paper, first, we propose a method of establishing secure communication channels between applications in embedded operating systems that run on multi-applet smart cards. Second, we enforce the high assurance using an intransitive noninterference security policy. Thirdly, we formalize the method through the Z language and create the formal specification of the proposed secure system. Finally, we verify its correctness using Rushby's unwinding theorem.

IoT systems are required to manage themselves to changes regarding their internal and external contexts. So, adaptability is a very important aspect in IoT software systems. The MAPE (Monitoring, Analysis, Planning, Execution) control loop model, inspired from the autonomic nervous system, has been identified as a crucial element for realizing self-adaptation in software systems. In fact, software design patterns provide architects and developers with reusable software elements helping them to master building complex software systems including several interconnected components. Complex self-adaptive systems require several architectural patterns in their design which leads to the need of architectural pattern composition. In this paper, we focus in modeling adaptability in IoT systems through a set of MAPE design patterns for decentralized control in self-adaptive systems and we propose an approach for composing them using a UML profile. Then, we propose formalizing the composition process using the Event-B method. In addition, we propose verifying adaptation properties based on the resulting formal specification. We illustrate our approach by modeling structural and behavioral features of the hybrid pattern resulting from the composition of two MAPE patterns and applied to the fall-detection ambient assisting living system for elderly people.

Software and systems engineering practitioners have the option to work with a very wide range of requirements specification methods. I view these as requirements languages. A subset of practitioners additionally has a compelling interest in using requirements methods that are suitable for very large-scale enterprise projects.1-4

Presents papers from the 2020 IEEE Conference on Requirements Engineering and the ACM/ IEEE 23rd International Conference on Model Driven Engineering Languages and Systems (MODELS 2020).

Blockchain- and smart-contract technology enhance the effectiveness and automation of business processes. The rising interest in the development of decentralized autonomous organizations (DAO) shows that blockchain technology has the potential to reform business and society. A DAO is an organization wherein business rules are encoded in smart-contract programs that are executed when specified rules are met. The contractual- and business semantics are sine qua non for drafting a legally-binding smart contract in DAO collaborations. Several smart-contract languages (SCLs) exist, such as SPESC, or Symboleo to specify a legally-binding contract. However, their primary focus is on designing and developing smart contracts with the cooperation of IT- and non-IT users. Therefore, this paper fills a gap in the state of the art by specifying a smart-legal-contract markup language (SLCML) for legal- and business constructs to draft a legally-binding DAO. To achieve the paper objective, we first present a formal SCL ontology to describe the legal- and business semantics of a DAO. Secondly, we translate the SCL ontology into SLCML, for which we present the XML schema definition. We demonstrate and evaluate our SLCML language through the specification of a real life-inspired Sale-of-Goods contract. Finally, the SLCML use-case code is translated into Solidity to demonstrate its feasibility for blockchain platform implementations.

Technological advances and increasing customer need for highly customized products have triggered a fourth industrial revolution. A digital revolution in the manufacturing industry is enforced by introducing smart devices and knowledge bases to form intelligent manufacturing information systems. One of the goals of the digital revolution is to allow flexibility of smart factories by automating shop floor changes based on the changes in input production processes and ordered products. In order to make this possible, a formal language to describe production processes is needed, together with a code generator for its models and an engine to execute the code on smart devices. Existing process modeling languages are not usually tailored to model production processes, especially if models are needed for automatic code generation. In this paper we propose a research on Industry 4.0 manufacturing using a Domain-Specific Modeling Language (DSML) within a Model-Driven Software Development (MDSD) approach to model production processes. The models would be used to generate instructions to smart devices and human workers, and gather a feedback from them during the process execution. A pilot comparative analysis of three modeling languages that are commonly used for process modeling is given with the goal of identifying supported modeling concepts, good practices and usage patterns.

The extent of formal verification methods applied to industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain, is rapidly changing the situation. Since the main area of DLSs' application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is required to ensure that the software implementation of the DLS nodes complies with this protocol. The verified software implementation of the protocol must run on a fairly reliable operating system. The so-called “smart contracts”, which are an important part of the applied implementations of specific business processes based on DLSs, must be verifiable as well. In this paper, we describe an ongoing industrial project that will result in a DLS verified at least at the four technological levels described above. We then share our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes.

A formal specification of access control yields a deeper understanding of any operating system, and facilitates performing security analysis of the OS. In this paper, we provide a comprehensive formal specification of access control in Android (ACiA). Prior work is limited in scope, furthermore, recent developments in Android concerning dynamic runtime permissions require rethinking of its formalization. Our formal specification includes three parts, the user-initiated operations (UIOs) and app-initiated operations (AIOs) - which are distinguished based on the initiating entity, and the URI permissions which are utilized in sharing temporary access to data. We also studied the evolution of URI permissions from API 10 (Gingerbread) to API 22 (Lollipop), and a brief discussion on this is included in the paper. Formalizing ACiA allowed us to discover many peculiar behaviors pertaining to ACiA. In addition to that, we discovered two significant issues with permissions in Android which were reported to Google.

The increasing complexity and criticality of industrial automation systems, embodied by the concept of Industry 4.0, which brings together concepts, such as cyber–physical systems, the Internet of Things, big data, and artificial intelligence, call for more formality in specifying the technology standards underlying these systems. We define in this article a formal model of an Industry 4.0 machine-to-machine communication protocol, Hermes, used in specifying electronic board transfers in an assembly line. Our analysis of the formal specification reveals that despite the robustness of the protocol, many testing scenarios have been ignored in the protocol standard and in particular, scenarios that include simultaneous machine errors. Therefore, this article paves the way for a better informed testing strategy in Industry 4.0 systems that implement the protocol.

With the development of blockchain technology, the fields of use of smart contracts are diversifying. Blockchain-based smart contracts are suitable in areas where integrity and transparency must be guaranteed with distributed ledger technology as the core. However, once the system is deployed, it cannot be modified, so it is important to ensure that the system works with the requirements and principles of the smart contract at the design stage. Therefore, in this paper, we aim to show that the system is accurate without contradictions/errors through formal verification using UPPAAL, a formal verification tool for the public descending auction system (Dutch Auction).

We present an executable formalism for clinical practice guidelines, with the aim of providing pervasive and evidence-based decision support to patients. Unlike traditional formalisms that capture the control flow between tasks, we focus on data flow, with tasks modeled as processes that execute in parallel. By parallelizing and distributing guideline knowledge, each device that constitutes the patient’s pervasive healthcare system can provide decision support independently, avoiding single points of failure. This distribution also enables dynamic system re-configurations, increasing its resilience against evolving requirements and changing communications environments. Our model recognizes four types of processes: Monitoring, Analysis, Decision and Effectuation. These processes were specified using (axiomatic) set theory and implemented as a set of libraries on top of Rosette, which supports execution of the formalism and verification of it using constraint solvers. The formalism was also tested by formalizing a complete clinical guideline for diabetes management, which yielded a Rosette program that was then tested on simulated patient data. The major point of clinical relevance is enhancing the quality and safety of decision support delivered to patients.

The cloud has several security and trust issues with the third-party provider. The blockchain-based cloud (BBC) system is an emerging technology that promises safe storage of big data on a cloud. The development of such a system needs requirements engineering (RE) in determining the requirements based on service-level agreements (SLAs). RE can provide a functional process to model and specify a SLA-based smart contract. The RE process for BBC ensures that the resulting SLA specifications are consistent, accurate, complete, verified, and validated. The RE process responds to the many challenges of the BBC and determines a novel direction to provide efficient and quality development of blockchainbased applications.

Audit logging provides post-facto analysis of runtime behavior for different purposes, including error detection, amelioration of system operations, and the establishment of security in depth. This necessitates some level of assurance on the quality of the generated audit logs, i.e., how well the audit log represents the events transpired during the execution. Information-algebraic techniques have been proposed to formally specify this relation and provide a framework to study correct audit log generation in a provable fashion. However, previous work fall short on how to guarantee this property of audit logging in concurrent environments. In this paper, we study an implementation model in a concurrent environment. We propose an algorithm that instruments a concurrent system according to a formal specification of audit logging requirements, so that any instrumented concurrent system guarantees correct audit log generation. As an application, we consider systems with microservices architecture, where logging an event by a microservice is conditioned on the occurrence of a collection of events that take place in other microservices of the system.

Controlling access to data is one of the primary purposes of security, especially when it comes to dealing with safety critical systems. In such systems, it is of paramount importance to rigorously define access control models. In this article, a correct-by-construction specification of RBAC using the Event-B formal method is proposed. The specification defines closely the model properties with the behavior aspect of RBAC as guards of events, which allows applying a priori verifications. Accordingly, the resulted specification is correct-by-construction and avoids the combinatorial explosion problem. As well, a number of refinement operations are performed leading to a specification with several abstraction levels, where each level implements selected RBAC entities. The approach is illustrated by an instantiation of a healthcare system.

In this position paper, we elaborate on the possibilities and needs to integrate Design Thinking into Requirements Engineering. We draw from our research and project experiences to compare what is understood as Design Thinking and Requirements Engineering considering their involved artifacts. We suggest three approaches for tailoring and integrating Design Thinking and Requirements Engineering with complementary synergies and point at open challenges for research and practice., Manuscript accepted for publication at a IEEE Software special issue on Design Thinking

PDF of Powerpoint Slides

Formal methods play an important role in testing and verifying software quality, especially in modern society with rapid technological updates. Learning-based techniques have been extensively applied to learn (a model or model-free) for formal verification and to learn system specifications, and resulted in numerous contributions. Due to the fact that adequate system models are often difficult to design manually and manual definition of specifications for such software systems gets infeasible, which motivate new research directions in learning models and/or specifications from observed system behaviors automatically. This paper mainly concentrates on learning-based techniques in formal methods area. An up-to-date overview of the current state-of-the-art in learning-based formal methods is provided in the paper. This paper is not a comprehensive survey of learning-based techniques in formal methods area, but rather as a survey of the taxonomy, applications and possible future directions in learning-based formal methods.

Smart contracts are a special type of programs running inside a blockchain. Immutable and transparent, they provide means to implement fault-tolerant and censorship-resistant services. Unfortunately, its immutability causes a serious challenge of ensuring that a business logic and implementation is correct upfront, before publishing in a blockchain. Several big accidents have indeed shown that users of this technology need special tools to verify smart contract correctness. Existing automated checkers are able to detect only well known implementation bugs, leaving the question of business logic correctness far aside. In this work, we present a symbolic model-checking technique along with a formal specification method for a subset of Solidity programming language that is able to express both state properties and trace properties; the latter constitutes a weak analogy of temporal properties. We evaluate the proposed technique on the MiniDAO smart contract, a young brother of notorious TheDAO. Our Proof-of-Concept was able to detect a non-trivial error in the business logic of this smart contract in a few seconds.

Runtime verification can be used to find bugs early, during software development, by monitoring test executions against formal specifications (specs). The quality of runtime verification depends on the quality of the specs. While previous research has produced many specs for the Java API, manually or through automatic mining, there has been no large-scale study of their bug-finding effectiveness. Our conference paper presented the first in-depth study of the bug-finding effectiveness of previously proposed specs. We used JavaMOP to monitor 182 manually written and 17 automatically mined specs against more than 18K manually written and 2.1M automatically generated test methods in 200 open-source projects. The average runtime overhead was under $$4.3{\times }$$. We inspected 652 violations of manually written specs and (randomly sampled) 200 violations of automatically mined specs. We reported 95 bugs, out of which developers already fixed or accepted 76. However, most violations, 82.81% of 652 and 97.89% of 200, were false alarms. Based on our empirical results, we conclude that (1) runtime verification technology has matured enough to incur tolerable runtime overhead during testing, and (2) the existing API specifications can find many bugs that developers are willing to fix; however, (3) the false alarm rates are worrisome and suggest that substantial effort needs to be spent on engineering better specs and properly evaluating their effectiveness. We repeated our experiments on a different set of 18 projects and inspected all resulting 742 violations. The results are similar, and our conclusions are the same.

Ontologies, as formal specifications of conceptualisation, are widely used in software engineering to manage software development, maintenance and security concerns. Recently, some ontology services were proposed for software vulnerability detection and showed to be effective. Some could detect more bugs compared to static analysis tools; some could predict hidden bugs based on ontology reasoning. In this paper, we review existing ontology-based services for vulnerability detection techniques, describe their main ideas and design principles, and provide background knowledge for further research in this area.

Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification., Formal Methods in System Design, 54 (3), ISSN:0925-9856, ISSN:1572-8102

Purpose Business process (BP) reengineering is defined as reinventing BPs either structurally or technically to achieve dramatic improvements in performance. In any business process reengineering (BPR) project, process modeling is used to reason about problems found in existing (as-is) process and helps to design target (to-be) process. BP model notation is a widely accepted standard for process modeling. “Expressiveness” and “missing formal semantics” are two problems reported to its modeling practices. In existing studies, solutions to these problems are also proposed but still have certain limitations. The paper aims to discuss this issue. Design/methodology/approach In proposed methodology, a meta-model is formally defined that is composed of commonly used modeling elements and their well-formedness rules to check for syntactic and structural correctness of process models. Proposed solution also check semantics of process models and allows to compare as-is and to-be process models for gap identification which is another important aspect of BPR. To achieve the first goal, Z specification is used to provide formal specifications of modeling constructs and their rules and Z3 (an SMT solver) is used for comparisons and verifying properties. Findings Proposed method addresses both “expressiveness” and “missing formal semantics” of BPR models. The results of its evaluation clearly indicate that using formally specified meta-model, BPR model is syntactically and structurally correct. Moreover, formal modeling of BPs in Z3 helped to compare processes and to check control flow properties. Research limitations/implications Although the proposed method is tested on an example that is widely used in BPR literature, the example is only covering modeling elements which are part of the proposed subset and are reported in literature as frequently used modeling elements. A separate detailed study is required to test it on more complex systems. Practical implications Specifying process models using Z specification and Z3 solver requires certain expertise. Originality/value The proposed method adds value to BPR body of knowledge as it proposes a method to ensure structural and syntactic correctness of models, highlighting the importance of verifying run time properties and providing a direction toward comparing process models for gap analysis.

This paper summarizes our efforts to aid human reasoning when verification fails through the use of two distinct Formalization Integrated Development Environments (F-IDEs) that we have developed. Both environments are modular and facilitate reasoning about the full behavior of object-based code. The first environment, referred to as the web-IDE, has been used for several years to teach aspects of formal specification and verification, including why and where verification conditions (VCs) arise and how to use them when verification fails. The second F-IDE, RESOLVE Studio, remains experimental, but is a more fully-fledged environment backed by a sequent-based VC generator that produces VCs with fewer extraneous givens. While the environments and VC generation techniques are necessarily language specific, the principles of alternative VC generation methods, F-IDE features, and observations about their impact on novices and experienced users are more generally applicable., In Proceedings AppFM 2021, arXiv:2111.07538

Cloud services must typically be distributed across a large number of machines in order to make use of multiple compute and storage resources. This opens the programmer to several sources of complexity such as concurrency, order of message delivery, lossy network, timeouts and failures, all of which impose a high cognitive burden. This paper presents evidence that technology inspired by formal-methods, delivered as part of a programming framework, can help address these challenges. In particular, we describe the experience of several engineering teams in Microsoft Azure that used the open-source Coyote Actor programming framework to build multiple reliable cloud services. Coyote Actors impose a principled design pattern that allows writing formal specifications alongside production code that can be systematically tested, without deviating from routine engineering practices. Engineering teams that have been using Coyote have reported dramatically increased productivity (in time taken to push new features to production) as well as services that have been running live for months without any issues in features developed and tested with Coyote.

A good graphical user interface (GUI) is crucial for an application's usability, so vendors and regulatory agencies increasingly place restrictions on how GUI elements should appear to and interact with users. Motivated by this concern, this paper presents a new technique (based on static analysis) for checking conformance between (Android) applications and GUI policies expressed in a formal specification language. In particular, this paper (1) describes a specification language for formalizing GUI policies, (2) proposes a new program abstraction called an _event-driven layout forest_, and (3) describes a static analysis for constructing this abstraction and checking it against a GUI policy. We have implemented the proposed approach in a tool called Venus, and we evaluate it on 2361 Android applications and 17 policies. Our evaluation shows that Venus can uncover malicious applications that perform ad fraud and identify violations of GUI design guidelines and GDPR laws.

Developing correct, scalable, and fault-tolerant distributed databases is hard and labor-intensive. The increasing complexity of such systems under modern cloud infrastructures, e.g., geo-replicated multi-partitioned datacenters, further limits the number of design alternatives that can be explored in practice. There is therefore a need for the formal analysis of both their qualitative properties, e.g., data consistency, and their quantitative properties, e.g., latency, at an early design stage. In this paper we use formal modeling and both standard and statistical model checking techniques to explore the design space of replicated RAMP (Read Atomic Multi-Partition) transactions for geo-replicated databases. Specifically, we develop in Maude formal, executable specifications of three replicated RAMP designs, two by the RAMP developers and one by us, and analyze their data consistency properties. We further transform the Maude models into probabilistic rewrite theories for statistical model checking w.r.t. performance properties. Our results: (i) are consistent with the conjectures made by the RAMP developers; (ii) uncover our promising new design that not only provides all crucial data consistency guarantees but also outperforms the other design alternatives.

Software Product Line deals with the development of product families for diverse market needs and includes feature model to describe the structure of the included products. Since feature model is lack of detailed specification of individual features, some behavior-oriented methods have been proposed to analyze the inner functionalities of features. But how these functions relate to the feature model remains a problem and a systematic approach is still needed to support the whole process of product family modeling. This paper provides a formal engineering approach to modeling product family where feature model evolves as individual features are formalized through informal, semi-formal and formal stages. For each stage, a set of evolvement rules are given to guide the refactoring of the feature model which will then serve as a basis for formal specifications of individual features. Such an iterative process repeats until achieving a feature model with consistent feature specifications. A case study is described to illustrate the effectiveness of our approach.

Cyber Physical Production Systems (CPPS) operate for a long time and face continuous and incremental changes to follow up varying requirements. Interdisciplinary engineering of CPPS is often subject to delay and cost overrun; and quality control may even fail due to the lack of efficient information exchange between multiple involved actors. We propose to integrate a formal requirement specification approach, namely Generalized Test Tables including tool support, into industrial workflows and present the approach through extended notations of Business Process Model and Notation (BPMN), namely BPMN++*, with the tool-coupling aspect. The suggested tooling enables automation engineers to follow the defined workflow systematically and communicate easier through the formally represented change requirement. The approach is demonstrated by two typical use cases of changing a CPPS’ control software and showing the result by means of an extended BPMN++ model exemplarily.

By 2030, over a half trillion devices will be connected to the internet. With so many devices providing a wide range of features, there is a need for a framework for innovation and reuse of Internet of Things (IoT) and Cyber-Physical Systems (CPS) capabilities. Such framework should facilitate the composition of capabilities and provide stakeholders means to reliably model and verify compositions. An IoT and CPS Composition Framework (ICCF) is proposed to achieve this goal. ICCF is based on the NIST CPS framework composition guidelines, intuitive composition semantics inspired from the mPlane protocol, and strong formal verification capabilities of the Temporal Logic of Actions (TLA) formal descriptors and tools. This paper demonstrates why such framework, semantics, and formal specification and verification components form a powerful and intuitive composition framework that satisfies different stakeholders concerns. To achieve this purpose, semantics and formal specification of the composition algebra were provided, a well-being composite capability within a smart building was specified, its prototype model in a formal verification tool was run, an analysis of the results of symbolic execution quantitatively and qualitatively was performed, and assessment of the trustworthiness of the composition was done. Lastly, implementation details were provided and proposed extensions to other domains such as smart transportation and smart health were discussed.

Protocol flaws such as the well-known Heartbleed bug, security and privacy issues or incomplete specifications, in general, pose risks to the direct users of a protocol and further stakeholders. Formal methods, such as Colored Petri Nets (CPNs), facilitate the design, development, analysis and verification of new protocols, the detection of flaws, and the mitigation of identified security risks. BlockVoke is a blockchain-based scheme that decentralizes certificate revocations, allows certificate owners and certificate authorities to revoke certificates and rapidly distributes revocation information. CPNs in particular are well-suited to formalize blockchain-based protocols—thus, in this work, we formalize the BlockVoke protocol using CPNs, resulting in a verifiable CPN model and a formal specification of the protocol. We utilize an agent-oriented modeling (AOM) methodology to create goal models and corresponding behavior interface models of BlockVoke. Subsequently, protocols semantics are defined, and the CPN models are derived and implemented using CPN Tools. Moreover, a full state-space analysis of the resulting CPN model is performed to derive relevant model properties of the protocol. The result is a complete and correct formal BlockVoke specification used to guide future implementations and security assessments.

Special Issue: Distributed Computing for Smart Networks: Recent Advances and Future Trends (DiCES‐N2019). AMMCS19. Security and Privacy in IoT Communication (IOTSEC19). SKG2019; International audience; Modeling and specifying correct software systems is a challenging task that can be supported by providing appropriate modeling abstractions. This article proposes an approach for graphical multiscale modeling of such systems using model transformation techniques. The approach is founded on a guided rule-based iterative modeling process ensuring controlled transition from a coarse-grained description to a fine-grained description. It provides also user-friendly graphical descriptions by extension of UML notations, hence preserving the common practices from software architectures design. The iterative design process is supported by a set of model transformation rules. The rules manage the refinement process (by adding or removing subsystems or by adding or removing details on a given subsystem) as a model transformation. Our approach is supported by a rule-based generator that implements the automatic transformation of UML diagrams into Event-B specifications allowing formal verification of their correctness properties, and relieving software architects of mastering formal techniques. To experiment and validate our approach, we consider a case study dedicated to the smart cities.

Methods and approaches in systems engineering are often based on the results of empirical observations or on individual success stories. Every real-world embedded system design stems from decisions based on an application domain knowledge that includes facts about some previous design practice. Evidently, such decisions relate to system architecture components, called in this paper as application patterns, which determine not only a required system behavior but also some presupposed implementation principles. Application patterns should respect those particular solutions that were successful in previous relevant design cases. While focused on the system architecture range that covers more than software components, the application patterns look in many features like wellknown software object-oriented design concepts such as reusable patterns (Coad and Yourdon, 1990), design patterns (Gamma et al., 1995), and frameworks (Johnson, 1997). By the way, there are also other related concepts such as use cases (Jacobson, 1992), architectural styles (Shaw and Garlan, 1996), or templates (Turner, 1997), which could be utilized for the purpose of this paper instead of introducing a novel notion. Nevertheless, application patterns can structure behavioral specifications and, concurrently, they can support architectural components specification reuse. Nowadays, industrial scale reusability frequently requires a knowledge-based support. Case-based reasoning (see e.g. Kolodner, 1993) can provide such a support. The method differs from other rather traditional procedures of Artificial Intelligence relying on case history: for a new problem, it strives for a similar old solution saved in a case library. Any case library serves as a knowledge base of a case-based reasoning system. The system acquires knowledge from old cases while learning can be achieved accumulating new cases. Solving a new case, the most similar old case is retrieved from the case library. The suggested solution of a new case is generated in conformity with the retrieved old case. This book chapter proposes not only how to represent a system’s formal specification as an application pattern structure of specification fragments, but also how to measure similarity of formal specifications for retrieval. In this chapter, case-based reasoning support to reuse is focused on specifications by finite-state and timed automata, or by state and timed-state

Modeling and verification of web services composition determines the execution flow of various web services used in conjunction. Existing techniques, such as, UML and testing are used successfully to describe the behavior of the web service system and find the bugs during the communication of the components. However, it is not always possible to identify bugs at all the stages. Formal specification and verification is an emerging technique for specifying the structural and functional property of the web service composition. Calculus of Communicating Systems (CCS) is a process-algebra used as a language for formal specification. In this article, we have utilized CCS for describing the behavioral specification of the web service system. The requirement of the system is captured through formulas or properties utilizing mu-calculus, and formally verified through Concurrency Work Bench of the New Century (CWB-NC) model checker tool.