Journal articles: 'Formal and semi-formal notation'

1

Dongmo, Cyrille, and John Andrew van der Poll. "Addressing the Construction of Z and Object-Z with Use Case Maps (UCMs)." International Journal of Software Engineering and Knowledge Engineering 24, no. 02 (2014): 285–327. http://dx.doi.org/10.1142/s0218194014500120.

Full text

Abstract:

A Use Case Map (UCM) is a scenario-based visual notation facilitating the requirements definition of complex systems. A UCM may be generated either from a set of informal requirements, or from a set of use cases normally expressed in natural language. Natural languages are, however, inherently ambiguous and as a semi-formal notation, UCMs have the potential to bring more clarity into the functional description of a system. It may furthermore eliminate possible errors in the user requirements. The semi-formal notation of UCMs aims to show how things work generally, but is not suitable to reason formally about system behavior. It is plausible, therefore, that the use of a UCM as an intermediate step may facilitate the construction of a formal specification. To this end this paper proposes a mechanism whereby a UCM may be translated into Object-Z.

APA, Harvard, Vancouver, ISO, and other styles

2

Kalashnikov, V. G., G. R. Gabidullina, S. M. Mukhametshin, A. S. Galimova, and A. M. Ableeva. "Formal and Psychological Aspects of Modern Business Notations." SHS Web of Conferences 93 (2021): 01015. http://dx.doi.org/10.1051/shsconf/20219301015.

Full text

Abstract:

The article discusses the features of the transition to the sixth technological order based on the digitalization of the economy, informatization and computerization of all spheres of human life. The conclusion is made about the influence of the ongoing phase shift of the social order on the social and psychological features of modern man. In particular, the increasing role of visual culture and visual (visual-logical) thinking and the corresponding graphic language is noted. The advantages of such a graphic language in terms of information capacity are noted. There is a growing interest in visual forms of modeling production systems in the form of business notations for the purpose of analyzing business processes for their modeling and controlling. The essence and features of the business notation system in various versions are considered. The possibility of combining different business notation systems as different ways of describing a managed object is emphasized. The article focuses on the use of business notation as a means of developing managerial thinking of managers as a multidimensional and contextual visual-logical process that meets the requirements of the modern information environment.

APA, Harvard, Vancouver, ISO, and other styles

3

Corradini, Flavio, Andrea Polini, and Barbara Re. "Inter-organizational business process verification in public administration." Business Process Management Journal 21, no. 5 (2015): 1040–65. http://dx.doi.org/10.1108/bpmj-02-2014-0013.

Full text

Abstract:

Purpose – Public services can be modelled, analysed and implemented using notations and tools for the business process (BP) abstraction. Applying such an explicit approach public administrations (PAs) can better react to the undergoing transformation in service provisioning and they can continuously improve service quality in order to satisfy citizens and business requests, while coping with decreasing budgets. The purpose of this paper is to discuss these issues. Design/methodology/approach – The proposed approach relies on using formal methods, in particular unfolding to analyse the correctness of BP. The paper also compares and selects mapping rules from semi-formal to formal modelling languages; these techniques are presented in the context of the BP Modelling Languages and Petri Net (PN). Findings – Main aim of this paper is to raise the need for formal verification of BP governing the interactions among PAs, which more and more need to be supported by ICT mechanisms, and then are not so much tolerant to errors and imperfections in the process specification. The paper illustrates the main motivations of such a work and it introduces a verification technique of a BP using a mapping of a high-level notation (such as BPMN 2.0) to a formal notation (such as PNs) for which formal analysis techniques can be adopted. In particular the verification step is implemented using an unfolding-based technique. Originality/value – The paper answers a call for further development of the body of knowledge on effective analysis of BPs, a rapidly emerging field of interest for large and ultra large scenarios, where a clear gap in literature exists. Than the paper shows that formal techniques are mature enough to be applied on real scenarios.

APA, Harvard, Vancouver, ISO, and other styles

4

Ciaccia, P., P. Ciancarini, and W. Penzo. "Formal Requirements and Design Specifications: The Clepsydra Methodology." International Journal of Software Engineering and Knowledge Engineering 07, no. 01 (1997): 1–42. http://dx.doi.org/10.1142/s0218194097000023.

Full text

Abstract:

The use of formal methods early in the development process has been advocated as a way of improving the quality of software products and their production process. Here we study the influence of a formal requirements document on the next phase in the software process, that is design. We suggest that formal design should coherently follow from formal requirements. We show that two different formal notations can be effectively used, one for writing requirements specification and one for design specification. We also consider how a design specification can be formally checked with respect to requirements specification. The notations we choose are well known: the Z notation for requirements and the Larch two-tiered language for design. We show how a number of tools based on these notations can be used to improve the quality of the documents produced during the development process.

APA, Harvard, Vancouver, ISO, and other styles

5

Aredo, Demissie. "A Framework for Semantics of UML Sequence Diagrams in PVS." JUCS - Journal of Universal Computer Science 8, no. (7) (2002): 674–97. https://doi.org/10.3217/jucs-008-07-0674.

Full text

Abstract:

This paper presents a framework for representing formal semantics of a subset of the Unified Modeling Language (UML) notation in a higher-order logic, more specifically semantics of UML sequence diagrams is encoded into the Prototype Verification System (PVS). The primary objective of our work is to make UML models amenable to rigorous analysis by providing their precise semantics. This approach paves a way for formal development of systems through a systematic transformation of UML models. This work is a part of a long-term vision to explore how the PVS tool set can be used to underpin practical tools for analyzing UML models. It contributes to the ongoing effort to provide mathematical foundation to UML notations, with the aim of clarifying the semantics of the language as well as supporting the development of semantically-based tools.

APA, Harvard, Vancouver, ISO, and other styles

6

Irawati, Eli. "transmission of resilience learning in the context of formal education an ethnomusicological review." Linguistics and Culture Review 5, S3 (2021): 1040–53. http://dx.doi.org/10.21744/lingcure.v5ns3.1664.

Full text

Abstract:

The existence and continuity of musical practice in the world, among others, is strongly influenced by transmission or inheritance. Therefore, local-traditional music in Indonesia that lives and develops in the midst of oral culture becomes important to study transmission. This study aims to determine the transmission process of learning in the Kalimantan Music class and find the right formula for delivering teaching materials. This research is qualitative research with an applied ethnomusicology approach. The method of collection is through observation, interviews and supported by documentation and literature searches. The research was conducted at the Department of Ethnomusicology, Faculty of Performing Arts, Indonesian Institute of the Arts, Yogyakarta. The study results indicate that it is important to incorporate learning models and strategies from the teacher to the Kalimantan Music class. They are practicing analytical-based learning methods in the context of a resilient society. Chunking-based strategies and formulas in memorizing songs or reports that are played are made into two notation systems, namely block notation and pronunciation-based notation, to make it easier for students to play music. Block notation formulas and pronunciation-based notations can be applied as a way of learning music in class.

APA, Harvard, Vancouver, ISO, and other styles

7

Zheng, Mingchun, Jiazhong Zhang, and Yanbing Wang. "Integrating a formal specification notation with HOOD." ACM SIGSOFT Software Engineering Notes 23, no. 5 (1998): 57–61. http://dx.doi.org/10.1145/290249.290265.

Full text

APA, Harvard, Vancouver, ISO, and other styles

8

France, R., A. Evans, K. Lano, and B. Rumpe. "The UML as a formal modeling notation." Computer Standards & Interfaces 19, no. 7 (1998): 325–34. http://dx.doi.org/10.1016/s0920-5489(98)00020-8.

Full text

APA, Harvard, Vancouver, ISO, and other styles

9

Waksler, Rachelle. "CV- versus X-Notation: A Formal Comparison." Annual Meeting of the Berkeley Linguistics Society 12 (May 15, 1986): 271. http://dx.doi.org/10.3765/bls.v12i0.1849.

Full text

APA, Harvard, Vancouver, ISO, and other styles

10

Lano, K., and H. Haughton. "Formal development in B abstract machine notation." Information and Software Technology 37, no. 5-6 (1995): 303–16. http://dx.doi.org/10.1016/0950-5849(95)99366-u.

Full text

APA, Harvard, Vancouver, ISO, and other styles

11

Dunsby, Jonathan. "The Formal Repeat." Journal of the Royal Musical Association 112, no. 2 (1987): 196–207. http://dx.doi.org/10.1093/jrma/112.2.196.

Full text

Abstract:

The music of many cultures is characterized by lengthy musical repetitions, especially where ceremony, text and dance determine the amount of music needed. In Western Classical music, formal repetition is an especially prominent feature. Considering the number of pieces in the customary concert repertoire which include repeats, even the casual observer may be surprised to see only a dozen column inches devoted to the topic in The New Grove Dictionary of 1980, with only five bibliographical references, all to peripheral sources. The dictionary entry is, however, well focused, with examples to support its general theme that ‘the evolution of the notation, its exact interpretation and the practice of making repeats .. raise certain problems, not all of which have obvious solutions’.

APA, Harvard, Vancouver, ISO, and other styles

12

Mancoridis, Spiros. "ISF: A Visual Formalism for Specifying Interconnection Styles for Software Design." International Journal of Software Engineering and Knowledge Engineering 08, no. 04 (1998): 517–40. http://dx.doi.org/10.1142/s0218194098000285.

Full text

Abstract:

We have developed a framework for specifying high-level software designs. The core of the framework is a very simple visual notation. This notation enables designers to document designs as labelled rectangles and directed edges. In addition to the notation, our framework features a supporting formalism, called ISF (Interconnection Style Formalism). This formalism enables designers to customize the simple design notation by specifying the type of entities, relations, legal configurations of entities and relations, as well as scoping rules of the custom notation. In this paper we present the formal definition of ISF and use ISF to specify two custom design notations. We also describe how ISF specifications, using deductive database technology, are used to generate supporting tools for these custom notations.

APA, Harvard, Vancouver, ISO, and other styles

13

Dongmo, Cyrille, and John Andrew Van der Poll. "An Improved User Requirements Notation (URN) Models’ Construction Approach." Systems 11, no. 6 (2023): 301. http://dx.doi.org/10.3390/systems11060301.

Full text

Abstract:

Semi-formal software techniques have been very successful in industry, government institutions and other areas such as academia. Arguably, they owe a large part of their success to their graphical notation, which is more human-oriented than their counterpart text-based and formal notation techniques. However, ensuring the consistency between two or more models is one of the known challenges of these techniques. This work looks closely at the specific case of the User Requirements Notation (URN) technique. Although the abstract model of URN provides for link elements to ensure the consistency between its two main components, namely, Goal-Oriented Requirement Language (GRL) and Use Case Maps (UCM), the effective implementation of such links is yet to be fully addressed. This paper performs a detailed analysis of the existing URN models construction process and proposes an improved process with some guidelines to ensure, by construction, the correctness and consistency of the GRL and UCM models. A case study is used throughout the paper to illustrate the suggested solution.

APA, Harvard, Vancouver, ISO, and other styles

14

Hussain, Shafiq, Peter Dunne, and Ghulam Rasool. "Formal Specification of Security Properties using Z Notation." Research Journal of Applied Sciences, Engineering and Technology 5, no. 19 (2013): 4664–70. http://dx.doi.org/10.19026/rjaset.5.4298.

Full text

APA, Harvard, Vancouver, ISO, and other styles

15

Felder, Miguel, and Mauro Pezzè. "A formal design notation for real-time systems." ACM Transactions on Software Engineering and Methodology 11, no. 2 (2002): 149–90. http://dx.doi.org/10.1145/505145.505146.

Full text

APA, Harvard, Vancouver, ISO, and other styles

16

Du, Guoping. "Parenthesis Notation." Journal of Research in Philosophy and History 5, no. 1 (2022): p44. http://dx.doi.org/10.22158/jrph.v5n1p44.

Full text

Abstract:

The formal language of a logical system usually contains several types of symbols. In infix notation, two different kinds of symbols are used to construct compound formula and to indicate the order of combination. The logical constants such as Ø, Ú are used to construct compound formula, and auxiliary symbols such as ( ) are used to indicate the order of a combination. In Polish notation, there is no need for auxiliary symbols such as ( ), and only one class of symbols, N, C, K, etc., is used as a conjunction to make it function as a parenthesis. Contrary to Polish notation, a new parenthesis notation is put forward in this paper. Parenthesis notation uses only parentheses, and empowers them the function of connectives. More importantly, it is proved in this paper that we can define logical constants such as propositional connectives, quantifiers, modal operators and temporal operators in the same formula by using only parenthesis, which can greatly simplify the initial connectives needed to construct the formal system.

APA, Harvard, Vancouver, ISO, and other styles

17

LAM, VITUS S. W. "FORMAL ANALYSIS OF BPMN MODELS: A NuSMV-BASED APPROACH." International Journal of Software Engineering and Knowledge Engineering 20, no. 07 (2010): 987–1023. http://dx.doi.org/10.1142/s0218194010005079.

Full text

Abstract:

Business Process Modeling Notation (BPMN) plays a significant role in the specification of business processes. To ascertain the validity of BPMN models, a disciplined approach to analyze their behavior is of particular interest to the field of business process management. This paper advocates a semantics-preserving method for transforming BPMN models into New Symbolic Model Verifier (NuSMV) language as a means to verify the models. A subset of BPMN is specified rigorously in the form of a mathematical model. With this foundation in place, the translation for the subset of BPMN notational elements is then driven by a set of formally defined rules. The practicality of our approach is exemplified using an on-line flight reservation service.

APA, Harvard, Vancouver, ISO, and other styles

18

Heitmeyer, Constance. "Formal Methods for Specifying, Validating, and Verifying Requirements." JUCS - Journal of Universal Computer Science 13, no. (5) (2007): 607–18. https://doi.org/10.3217/jucs-013-05-0607.

Full text

Abstract:

This paper describes the specification, validation and verification of system and soft-ware requirements using the SCR tabular method and tools. An example is presented to illustrate the SCR tabular notation, and an overview of each of the ten tools in the SCR toolset is presented.

APA, Harvard, Vancouver, ISO, and other styles

19

MOTSCHNIG-PITRIK, RENATE, and JOHN MYLOPOULOS. "CLASSES AND INSTANCES." International Journal of Cooperative Information Systems 01, no. 01 (1992): 61–92. http://dx.doi.org/10.1142/s0218215792000040.

Full text

Abstract:

The power of any information system technology is delimited by the expressiveness of the notation used to represent information. Classification constitutes a fundamental notational structuring mechanism and, not surprisingly, is supported in one form or another by many formal notations intended for data or knowledge modelling. This paper presents an overview of various manifestations of classification mechanisms. Further, characteristic features of classification, such as the form of inheritance allowed from classes to instances, having single or multiple classifications and the structure of the classification hierarchy are identified, discussed, and contrasted. The paper also describes the classification mechanism offered by the knowledge representation language Telos. In Telos, classification is stratified and applicable not only to objects but also to (binary) relationships. The paper argues that these features lead to a more expressive notation, acquired at relatively modest conceptual and computational costs.

APA, Harvard, Vancouver, ISO, and other styles

20

CHEN-BURGER, YUN-HEH, DAVID ROBERTSON, and JUSSI STADER. "FORMAL SUPPORT FOR AN INFORMAL BUSINESS MODELLING METHOD." International Journal of Software Engineering and Knowledge Engineering 10, no. 01 (2000): 49–68. http://dx.doi.org/10.1142/s0218194000000055.

Full text

Abstract:

Business modelling methods are popular but, since they operate primarily in the early stages of software lifecycles, most are informal. This paper describes how we have used a conventional formal notation (first order predicate logic) in combination with automated support tools to replicate the key components of an established, informal, business modelling method: IBM's Business System Development Method (BSDM). We describe the knowledge which we represent formally at each stage in the method and explain how the move from informal to formal representation allows us to provide guidance and consistency checking during the development lifecycle of the model. It also allows us to extend the original method to a model execution phase which is not described in the original informal method. The role of the formal notation in this case is not to provide a formal semantics for BSDM but to provide a framework for sharing the information supplied at different modelling stages and which we can supplement with simple forms of automated analysis.

APA, Harvard, Vancouver, ISO, and other styles

21

Ainley, Janet. "Purposeful contexts for formal notation in a spreadsheet environment." Journal of Mathematical Behavior 15, no. 4 (1996): 405–22. http://dx.doi.org/10.1016/s0732-3123(96)90025-5.

Full text

APA, Harvard, Vancouver, ISO, and other styles

22

GARGOURI, BILEL, MOHAMED JMAIEL, and ABDELMAJID BEN HAMADOU. "An approach to the formal specification of lingware." Natural Language Engineering 9, no. 3 (2003): 211–30. http://dx.doi.org/10.1017/s1351324902003030.

Full text

Abstract:

This paper has two purposes. First, it suggests a formal approach for specifying and verifying lingware. This approach is based on a unified notation of the main existing formalisms for describing linguistic knowledge (i.e. Formal Grammars, Unification Grammars, HPSG, etc.) on the one hand, and the integration of data and processing on the other. Accordingly, a lingware specification includes all related aspects in a unified framework. This facilitates the development of a lingware system, since one has to follow a single development process instead of two separate ones. Secondly, it presents an environment for the formal specification of lingware, based on the suggested approach, which is neither restricted to a particular kind of application nor to a particular class of linguistic formalisms. This environment provides interfaces enabling the specification of both linguistic knowledge and functional aspects of a lingware system. Linguistic knowledge is specified with the usual grammatical formalisms, whereas functional aspects are specified with a suitable formal notation. Both descriptions will be integrated into the same framework to obtain a complete requirement specification that can be refined towards an executable program.

APA, Harvard, Vancouver, ISO, and other styles

23

Dunning, David E. "The logic of the nation: Nationalism, formal logic, and interwar Poland." Studia Historiae Scientiarum 17 (December 12, 2018): 207–51. http://dx.doi.org/10.4467/2543702xshs.18.009.9329.

Full text

Abstract:

Between the World Wars, a robust research community emerged in the nascent discipline of mathematical logic in Warsaw. Logic in Warsaw grew out of overlapping imperial legacies, launched mainly by Polish-speaking scholars who had trained in Habsburg universities and had come during the First World War to the University of Warsaw, an institution controlled until recently by Russia and reconstructed as Polish under the auspices of German occupation. The intellectuals who formed the Warsaw School of Logic embraced a patriotic Polish identity. Competitive nationalist attitudes were common among interwar scientists – a stance historians have called “Olympic internationalism,” in which nationalism and internationalism interacted as complementary rather than conflicting impulses. One of the School’s leaders, Jan Łukasiewicz, developed a system of notation that he promoted as a universal tool for logical research and communication. A number of his compatriots embraced it, but few logicians outside Poland did; Łukasiewicz’s notation thus inadvertently served as a distinctively national vehicle for his and his colleagues’ output. What he had intended as his most universally applicable invention became instead a respected but provincialized way of writing. Łukasiewicz’s system later spread in an unanticipated form, when postwar computer scientists found aspects of its design practical for working under the specific constraints of machinery; they developed a modified version for programming called “Reverse Polish Notation” (RPN). RPN attained a measure of international currency that Polish notation in logic never had, enjoying a global career in a different discipline outside its namesake country. The ways in which versions of the notation spread, and remained or did not remain “Polish” as they traveled, depended on how readers (whether in mathematical logic or computer science) chose to read it; the production of a nationalized science was inseparable from its international reception.

APA, Harvard, Vancouver, ISO, and other styles

24

Gibert, Karina, and Yaroslav Hernandez-Potiomkin. "A Unified Formal Framework for Factorial and Probabilistic Topic Modelling." Mathematics 11, no. 20 (2023): 4375. http://dx.doi.org/10.3390/math11204375.

Full text

Abstract:

Topic modelling has become a highly popular technique for extracting knowledge from texts. It encompasses various method families, including Factorial methods, Probabilistic methods, and Natural Language Processing methods. This paper introduces a unified conceptual framework for Factorial and Probabilistic methods by identifying shared elements and representing them using a homogeneous notation. The paper presents 12 different methods within this framework, enabling easy comparative analysis to assess the flexibility and how realistic the assumptions of each approach are. This establishes the initial stage of a broader analysis aimed at relating all method families to this common framework, comprehensively understanding their strengths and weaknesses, and establishing general application guidelines. Also, an experimental setup reinforces the convenience of having harmonized notational schema. The paper concludes with a discussion on the presented methods and outlines future research directions.

APA, Harvard, Vancouver, ISO, and other styles

25

Líska, Miroslav, and Pavol Navrat. "SPEM ontology as the semantic notation for method and process definition in the context of SWEBOK." Computer Science and Information Systems 8, no. 2 (2011): 299–315. http://dx.doi.org/10.2298/csis101230011l.

Full text

Abstract:

The Guide to the Software Engineering Body of Knowledge (SWEBOK) provides a consensually validated characterization of the bounds of the software engineering discipline and to provide a topical access to the Body of Knowledge supporting that discipline. The topic ?Notation for Process Definition? references selected notations appropriate for software process definition. However all of them have weakly defined semantics, thus is not possible to use formal techniques for process model creation, validation etc. In this work we present created Software and Systems Process Engineering Meta-Model (SPEM) Ontology that improves the lack of mentioned process notations. The SPEM Ontology constitutes a semantic notation that provides concepts for knowledge based software process engineering. The work also discusses utilization of such semantic notation in other selected SWEBOK topics, the Software Project Planning, the Software Project Enactment, and the Verification and Validation.

APA, Harvard, Vancouver, ISO, and other styles

26

Prasetya, I. S. W. B., and S. D. Swierstra. "Formal design of self-stabilizing programs." Journal of High Speed Networks 14, no. 1 (2005): 59–83. https://doi.org/10.3233/hsn-2005-259.

Full text

Abstract:

Distributed algorithms, self-stabilizing systems in particular, are often too delicate to be argued informally. Formal proofs are much more reliable, but unfortunately are often long and complicated. Some of the complication is inherent, but some is also the result of poor notation and formalism which is not abstract enough. Improving them would make formal proofs easier to write and to understand, which will also make them less error prone. In this spirit, this paper proposes an extension of the logic UNITY with a number of new operators to model self-stabilization and a formalization of a number of useful design strategies. They should enhance the formalism offered by UNITY with better abstraction to specify and reason about self-stabilization.

APA, Harvard, Vancouver, ISO, and other styles

27

Bénabou, Jean. "Fibered categories and the foundations of naive category theory." Journal of Symbolic Logic 50, no. 1 (1985): 10–37. http://dx.doi.org/10.2307/2273784.

Full text

Abstract:

Any attempt to give “foundations”, for category theory or any domain in mathematics, could have two objectives, of course related.(0.1) Noncontradiction: Namely, to provide a formal frame rich enough so that all the actual activity in the domain can be carried out within this frame, and consistent, or at least relatively consistent with a well-established and “safe” theory, e.g. Zermelo-Frankel (ZF).(0.2) Adequacy, in the following, nontechnical sense:(i) The basic notions must be simple enough to make transparent the syntactic structures involved.(ii) The translation between the formal language and the usual language must be, or very quickly become, obvious. This implies in particular that the terminology and notations in the formal system should be identical, or very similar, to the current ones. Although this may seem minor, it is in fact very important.(iii) “Foundations” can only be “foundations of a given domain at a given moment”, therefore the frame should be easily adaptable to extensions or generalizations of the domain, and, even better, in view of (i), it should suggest how to find meaningful generalizations.(iv) Sometimes (ii) and (iii) can be incompatible because the current notations are not adapted to a more general situation. A compromise is then necessary. Usually when the tradition is very strong (ii) is predominant, but this causes some incoherence for the notations in the more general case (e.g. the notation f(x) for the value of a function f at x obliges one, in category theory, to denote the composition of arrows (f, g) → g∘f, and all attempts to change this notation have, so far, failed).

APA, Harvard, Vancouver, ISO, and other styles

28

Liu, Shaoying. "A Formal Definition of FRSM and Applications." International Journal of Software Engineering and Knowledge Engineering 08, no. 02 (1998): 253–81. http://dx.doi.org/10.1142/s0218194098000145.

Full text

Abstract:

FRSM (Formal Requirements Specification Method) is a structured formal language and method for requirements analysis and specification construction based on data flow analysis. It uses a formalized DeMarco data flow diagram to describe the overall structure of systems and a VDM-SL like formal notation to describe precisely the functionality of components in the diagrams. This paper first describes the formal syntax and semantics of FRSM and then presents an example of using the axiom and inference rules given in the definition of the formal semantics for checking consistency of specifications. A case study of applying FRSM to a practical example is described to demonstrate the principle of constructing requirements specifications and to uncover the benefits and deficiencies of FRSM.

APA, Harvard, Vancouver, ISO, and other styles

29

Kodagoda, Nuwan, and Koliya Pulasinghe. "Comparision Between Features of CbO based Algorithms for Generating Formal Concepts." International Journal of Conceptual Structures and Smart Applications 4, no. 1 (2016): 1–34. http://dx.doi.org/10.4018/ijcssa.2016010101.

Full text

Abstract:

Formal Concept Analysis provides the mathematical notations for representing concepts and concept hierarchies making use of order and lattice theory. This has now been used in numerous applications which include software engineering, linguistics, sociology, information sciences, information technology, genetics, biology and in engineering. The algorithms derived from Kustenskov's CbO were found to provide the most efficient means of computing formal concepts in several research papers. In this paper key enhancements to the original CbO algorithms are discussed in detail. The effects of these key features are presented in both isolation and combination. Eight different variations of the CbO algorithms highlighting the key features were compared in a level playing field by presenting them using the same notation and implementing them from the notation in the same way. The three main enhancements considered are the partial closure with incremental closure of intents, inherited canonicity test failures and using a combined depth first and breadth first search. The algorithms were implemented in an un-optimized way to focus on the comparison on the algorithms themselves and not on any efficiencies provided by optimizing code. The main contribution of this paper is the complete comparison of the three main enhancements used in recent variations of the CbO based algorithms. The main findings were that there is a significant performance improvement partial closure with incremental closure of intents is used in isolation. However, there is no significant performance improvement when the depth and breadth first search or the inherited canonicity test failure feature is used in isolation. The inherited canonicity test failure needs to be combined with the combined depth and breadth first feature to obtain a performance increase. Combining all the three enhancements brought the best performance.

APA, Harvard, Vancouver, ISO, and other styles

30

Yeung, W. "Checking Consistency between UML Class and State Models Based on CSP and B." JUCS - Journal of Universal Computer Science 10, no. (11) (2004): 1540–58. https://doi.org/10.3217/jucs-010-11-1540.

Full text

Abstract:

The B Abstract Machine Notation (AMN) and the notation of Communicating Sequential Processes (CSP) have previously been applied to formalise the UML class and state diagrams, respectively. This paper discusses their integrated use in checking the consistency between the two kinds of UML diagrams based on some recent results of research in integrated formal methods. Through a small information system example, the paper illustrates a clear-cut separation of concerns in employing the two formal methods. Of particular interest is the treatment of recursive calls within a single class of objects.

APA, Harvard, Vancouver, ISO, and other styles

31

Couto, Luís Diogo, Peter Gorm Larsen, Miran Hasanagić, Georgios Kanakis, Kenneth Lausdahl, and Peter W. V. Tran-Jørgensen. "Towards Enabling Overture as a Platform for Formal Notation IDEs." Electronic Proceedings in Theoretical Computer Science 187 (August 14, 2015): 14–27. http://dx.doi.org/10.4204/eptcs.187.2.

Full text

APA, Harvard, Vancouver, ISO, and other styles

32

orC.I, Ejiof, and Mgbea fuluike.I.J. "Hospital Management System (HMS): A Formal Approach using Z-notation." International Journal of Computer & Organization Trends 7, no. 6 (2017): 11–13. http://dx.doi.org/10.14445/22492593/ijcot-v7i6p302.

Full text

APA, Harvard, Vancouver, ISO, and other styles

33

Finney, K. "Mathematical notation in formal specification: too difficult for the masses?" IEEE Transactions on Software Engineering 22, no. 2 (1996): 158–59. http://dx.doi.org/10.1109/32.485225.

Full text

APA, Harvard, Vancouver, ISO, and other styles

34

Douibi, Halima, and Faiza Belala. "Design Patterns Formal Composition and Analysis." International Journal of Information Technologies and Systems Approach 12, no. 2 (2019): 1–21. http://dx.doi.org/10.4018/ijitsa.2019070101.

Full text

Abstract:

Informal description of design patterns was adopted to facilitate their understanding by software developers. However, these descriptions lead to ambiguities limiting their successful use in real applications. Recently, several formal methods have been employed to guarantee precise specification of design pattern elements without insisting on their behavior. The main goal of this article is to propose a rewriting logic-based framework for enhancing formal description and reasoning on design patterns composition. The proposed model is integrated and executed under Maude using K-Maude tool. It allows first to associate a meta model notation, according to MDA approach, to all design patterns elements and then, a Maude semantic basis for specifying both their structural and dynamic aspects, is given. In particular, it will be shown how the authors' combined modeling approach is exploited for defining a set of operations on patterns, and how it will be used to formal analyze patterns composition.

APA, Harvard, Vancouver, ISO, and other styles

35

HILAIRE, VINCENT, PABLO GRUER, ABDER KOUKAM, and OLIVIER SIMONIN. "FORMAL SPECIFICATION APPROACH OF ROLE DYNAMICS IN AGENT ORGANISATIONS: APPLICATION TO THE SATISFACTION-ALTRUISM MODEL." International Journal of Software Engineering and Knowledge Engineering 17, no. 05 (2007): 615–41. http://dx.doi.org/10.1142/s0218194007003392.

Full text

Abstract:

This article deals with the problem of dynamic role-playing in Multi-Agent organisations. The approach presented uses a formal specification notation and is based upon a formal framework which defines the concepts of role, interaction and organisation. Within this framework the problem of dynamic role-playing specification is related to the merging of specifications. The formal notation used composes Object-Z and Statecharts. The main features of this approach are: enough expressive power to represent Multi-Agents dynamic aspects, tools for specification analysis and mechanisms allowing the refinement of a high level specification into a low level specification which can be easily implemented. The last part of this paper presents an application with the specification of a reactive and cooperative MAS model named Satisfaction Altruism. An analysis of the specification validates the agents' behaviours.

APA, Harvard, Vancouver, ISO, and other styles

36

Rábová, Ivana. "The formal logic of business rules." Acta Universitatis Agriculturae et Silviculturae Mendelianae Brunensis 55, no. 6 (2007): 133–40. http://dx.doi.org/10.11118/actaun200755060133.

Full text

Abstract:

Identification of improvement areas and utilization of information and communication technologies have gained value and priority in our knowledge driven society. Rules define constraints, conditions and policies of how the business processes are to be performed but they also affect the behavior of the resource and facilitate strategic business goals achieving. They control the business and represent business knowledge. The research works about business rules show how to specify and classify business rules from the business perspective and to establish an approach to managing them that will enable faster change in business processes and other business concepts in all areas of the business. In concrete this paper deals with four approaches to business rules formalization, i. e. notation of OCL, inference rules, decision table and predicate logic and with their general evaluation. The article shows also the advantages and disadvantages of these approaches of formalization. They are the example of every mentioned approach.

APA, Harvard, Vancouver, ISO, and other styles

37

McCaffrey, Tony, and Percival G. Matthews. "An Emoji Is Worth a Thousand Variables." Mathematics Teacher 111, no. 2 (2017): 96–102. http://dx.doi.org/10.5951/mathteacher.111.2.0096.

Full text

APA, Harvard, Vancouver, ISO, and other styles

38

Semenov, Vitaly Adolfovich, Semen Vasilyevich Arishin, and Georgii Vitalyevich Semenov. "Formal Rules to Produce Object Notation for EXPRESS Schema-Driven Data." Proceedings of the Institute for System Programming of the RAS 33, no. 5 (2021): 7–24. http://dx.doi.org/10.15514/ispras-2021-33(5)-1.

Full text

Abstract:

Recently, product data management systems (PDM) are widely used to conduct complex multidisciplinary projects in various industrial domains. The PDM systems enable teams of designers, engineers, and managers to remotely communicate on a network, exchange and share common product information. To integrate CAD/CAM/CAE applications with the PDM systems and ensure their interoperability, a dedicated family of standards STEP (ISO 10303) has been developed and employed. The STEP defines an object-oriented language EXPRESS to formally specify information schemas as well as file formats to store and transfer product data driven by these schemas. These are clear text encoding format SPF and STEP-XML. Nowadays, with the development and widespread adoption of Web technologies, the JSON language is getting increasingly popular due to it being apropos for the tasks of object-oriented data exchange and storage, as well as its simple, easy to parse syntax. The paper explores the topic of the suitability of the JSON language for the unambiguous representation, storage and interpretation of product data. Under the assumption that the product data can be described by arbitrary information schemas in EXPRESS, formal rules for the producing JSON notation are proposed and presented. Explanatory examples are provided to illustrate the proposed rules. The results of computational experiments conducted confirm the advantages of the JSON format compared to SPF and STEP-XML, and motivate its widespread adoption when integrating software applications.

APA, Harvard, Vancouver, ISO, and other styles

39

DONG, JIN SONG, PING HAO, and BRENDAN MAHONY. "FORMAL DESIGNS FOR EMBEDDED AND HYBRID SYSTEMS." International Journal of Software Engineering and Knowledge Engineering 15, no. 02 (2005): 373–78. http://dx.doi.org/10.1142/s0218194005002117.

Full text

Abstract:

The design of embedded and hybrid systems requires powerful mechanisms for modeling data, state, concurrency and real-time behaviour. The {first} part of this paper illustrates a powerful design notation Timed Communicating Object Z (TCOZ) that has both channel based and sensor/actuator based interfaces. We believe that TCOZ is well suited for presenting more complete and coherent design models for complex embedded and hybrid systems. However, the challenge is how to analyze and check these models with tools support. One effective approach is to project (transform) the design models into multiple domains, then to use existing specialized tools in those domains to perform the checking and analyzing tasks. The second part of this paper demonstrates one particular projection from TCOZ designs to Timed Automata (TA) models so that TA model checkers can be used to check time related properties.

APA, Harvard, Vancouver, ISO, and other styles

40

Stanimirovic, Predrag, Predrag Krtolica, and Rade Stanojevic. "A non-recursive algorithm for polygon triangulation." Yugoslav Journal of Operations Research 13, no. 1 (2003): 61–67. http://dx.doi.org/10.2298/yjor0301061s.

Full text

Abstract:

In this paper an algorithm for the convex polygon triangulation based on the reverse Polish notation is proposed. The formal grammar method is used as the starting point in the investigation. This idea is "translated" to the arithmetic expression field enabling application of the reverse Polish notation method. .

APA, Harvard, Vancouver, ISO, and other styles

41

BOUDIAF, NOURA, FARID MOKHATI, and MOURAD BADRI. "SUPPORTING FORMAL VERIFICATION OF DIMA MULTI-AGENTS MODELS: TOWARDS A FRAMEWORK BASED ON MAUDE MODEL CHECKING." International Journal of Software Engineering and Knowledge Engineering 18, no. 07 (2008): 853–75. http://dx.doi.org/10.1142/s021819400800391x.

Full text

Abstract:

Model Checking based verification techniques represent an important issue in the field of concurrent systems quality assurance. The lack of formal semantics in the existing formalisms describing multi-agents models combined with multi-agents systems complexity are sources of several problems during their development process. The Maude language, based on rewriting logic, offers a rich notation supporting formal specification and implementation of concurrent systems. In addition to its modeling capacity, the Maude environment integrates a Model Checker based on Linear Temporal Logic (LTL) for distributed systems verification. In this paper, we present a formal and generic framework (DIMA-Maude) supporting formal description and verification of DIMA multi-agents models.

APA, Harvard, Vancouver, ISO, and other styles

42

Al-Khatib, Saleh. "The Formal Notation of Some Phonological Processes in the Holy Quran." Journal of King Abdulaziz University-Educational Sciences 16, no. 1 (2003): 25–37. http://dx.doi.org/10.4197/edu.16-1.2.

Full text

APA, Harvard, Vancouver, ISO, and other styles

43

Miyazawa, Alvaro, and Ana Cavalcanti. "SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java." Electronic Proceedings in Theoretical Computer Science 209 (June 4, 2016): 71–86. http://dx.doi.org/10.4204/eptcs.209.6.

Full text

APA, Harvard, Vancouver, ISO, and other styles

44

Barańska, Anna M., and Konrad Eckes. "A formal notation of legal rules applicable in the local space." Geoinformatica Polonica 23 (December 19, 2024): 101–12. https://doi.org/10.4467/21995923gp.24.008.20900.

Full text

Abstract:

In addition to the commonly known stable legal relationships between persons or institutions and fragments of the Earth's surface (real estate), there are widely applied ad hoc relationships to real space, with significantly varying durations. They are a function of acquired rights and remain valid for a strictly defined period of time. They are common in everyday life and take on diverse forms, the basic attribute of which is a reference to a broadly understood fragment of geographical space. Emerging technological achievements, such as digitisation of payments, algorithmisation of procedures, identification of documents and people, autonomous traffic and artificial intelligence - pose a challenge to provide ad hoc relationships to space with formalised notation. The problem of formal notation of legal rules applicable in local space will be presented on the example of the right of entry to the university campus, together with local traffic and parking rules. The space is divided into zones and then into smaller units – parking spaces, according to the hierarchical structure. Social groups that have relationships with these zones are also formed into hierarchical sets. Individual groups have different rights to space – hierarchically – at the zone level. The established hierarchy is the first factor considered. The second factor is variability over time. Relationships to local space change over time, most often in a cyclical form. It can therefore be concluded that in this case the law is a function of time. Parking spaces, as objects in spatial sets, are occupied randomly and subsequent users must start the procedure of searching the remaining objects belonging to the set. This procedure has been written in the form of a flowchart and graph. Objects removed from the set (as they are occupied) may randomly return, so for the purposes of effective searching, this process is presented as repeatable – as a whole or locally (cascading search). The third aspect considered are differences in the way users move around the local road network and in elementary spatial fields. The network structure is represented by intersections, which are noted as node matrices. In order to define how to behave in the local space, a list of rules was prepared and standardised. From a practical point of view, a form of prohibition is advantageous because it can be logically linked to a list (set) of consequences. Following these assumptions, the general form of the behavioural test algorithm was formulated. The presented issues demonstrate complex relationships to space and its integrating rule in relation to legal rules. This approach to law allows for space management using IT methods. The notation of the spatial structure and of legal relationships related to time enable the definition of rules of conduct for diverse groups of local societies. Dissimilarity from equality of law for all and stability over time, occurs in local environments and raises the relationships between community, space and time to a higher level of generality.

APA, Harvard, Vancouver, ISO, and other styles

45

Zafar, N. A. "Formal specification and validation of railway network components using Z notation." IET Software 3, no. 4 (2009): 312. http://dx.doi.org/10.1049/iet-sen.2008.0082.

Full text

APA, Harvard, Vancouver, ISO, and other styles

46

da Rocha Costa, Antônio Carlos. "Situated Ideological Systems: A Formal Concept, a Computational Notation, some Applications." Axiomathes 27, no. 1 (2016): 15–78. http://dx.doi.org/10.1007/s10516-016-9293-3.

Full text

APA, Harvard, Vancouver, ISO, and other styles

47

Semenov, V. A., S. V. Arishin, and G. V. Semenov. "Formal Rules to Produce Object Notation for EXPRESS Schema-Driven Data." Programming and Computer Software 48, no. 7 (2022): 455–68. http://dx.doi.org/10.1134/s0361768822070076.

Full text

APA, Harvard, Vancouver, ISO, and other styles

48

Bastide, R�mi, Ousmane Sy, and Philippe Palanque. "A formal notation and tool for the engineering of CORBA systems." Concurrency: Practice and Experience 12, no. 14 (2000): 1379–403. http://dx.doi.org/10.1002/1096-9128(20001210)12:14<1379::aid-cpe514>3.0.co;2-b.

Full text

APA, Harvard, Vancouver, ISO, and other styles

49

El Miloudi, Khadija, and Aziz Ettouhami. "A Multiview Formal Model of Use Case Diagrams Using Z Notation: Towards Improving Functional Requirements Quality." Journal of Engineering 2018 (December 2, 2018): 1–9. http://dx.doi.org/10.1155/2018/6854920.

Full text

Abstract:

We propose a new formal model of UML use case diagram using Z notation to address some of its shortcomings. UML use case diagram has therefore become commonly used to structure functional requirements and the greatest challenge facing the software developer nowadays is to deliver a high quality product meeting customers’ requirements. However, the major disadvantage of UML models is their imprecision. In addition, they are basically in a form of semiformal modelling representations and associated natural language requirements and lack any mechanism to rigorously check consistency which results in its models being subject to ambiguity. This paper reports on the first formal modelling approach of use case diagrams in a multiview context. The approach is divided into two steps. In the first step, a formal model of UML use case diagram is proposed using Z notation. Then, a multiview consistency checking is presented. This approach guarantees software consistency, improving requirements quality.

APA, Harvard, Vancouver, ISO, and other styles

50

Kowalska-Zając, Ewa. "Is notational “fingerprint” still possible? A few comments on the idiomaticity of the 20th-century notation." Polski Rocznik Muzykologiczny 22, no. 1 (2024): 164–83. https://doi.org/10.2478/prm-2024-0005.

Full text

Abstract:

Abstract The discussion started by the author will be restricted to the Polish compositional output of the second half of the 20th century, with the subject matter covering the idiomaticity of notation as a consequence of modifications arising from the introduction of new compositional techniques and authors’ original formal solutions. The “fingerprint” in the title of the article encompasses not only individual features of notation, in the form of a specific font or shape of particular elements of the notational system, but also solutions of a systemic nature, allowing to copy the texture or form of a composition in a concise manner. The idiomaticity of notation also means visual attractiveness of scores, created under the influence of avant-garde trends in the time when originality in that respect was not limited yet, or even eliminated, by widespread and unifying notation of music notation processors. An additional motivator behind this attempt to characterize the phenomenon was a need for a nostalgic comeback to the decades when the only limitation regarding notation were the limits of a composer’s imagination, and published scores (mainly in the form of facsimiles) bore the composer’s distinctive fingerprint.

APA, Harvard, Vancouver, ISO, and other styles

Journal articles on the topic 'Formal and semi-formal notation'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles