A UML 2.0 Activity Diagrams/CSP Integrated Approach for Modeling and Verification of Software Systems

This paper proposes an approach integrating UML 2.0 Activity Diagrams (UML2-AD) and Communicating Sequential Process (CSP) for modeling and verication of software systems. A UML2-AD is used for modeling a software system while CSP is used for verication purposes. The proposed approach consists of another way of transforming UML2-AD models to Communicating Sequential Process (CSP) models. It focuses also on checking the correctness of some properties of the transformation itself. These properties are specified using Linear Temporal Logic (LTL) and verified using the GROOVE model checker. This approach is based on Model Driven Engineering (MDE). The meta-modelling is realized using AToMPM tool while the model transformation and the correctness of its properties are realized using GROOVE tool. Finally, we illustrated this approach through a case study.

PERENCANAAN FRAMWORK ZACHMAN DALAM ENTERPRISE RESOURSE PLANNING SISTEM INFORMASI PADA PT SARANA PEMBAGUNAN PALEMBANG JAYA (SP2J)

In the design of Enterprice Resource Planning (ERP), it takes palnning organized, since the ERP aimed ti integrate the entire process that exists in different funcsional domains of the company, inter-deparmental, or between diffrent locations. This research aims to design a blueprint for gentting application esign application in the module inventory Managamnt (IM) Zachman Framwork (ZF) is a framwork that can chart the artifact information architecture in an (Planner,Owner Perspective Perspective, Designer, Builder, Implementer Perspective perspective) appropriate abstraction object (What, How, Where, Who, When, and Why). To standardize information architechure artifacts used modeling standard UML 2.0 approach so it able to improve the desription of the standard Model of ZF be Driven Architecture. For testing the results of design has developed ERP software IM appling model driven design that is able to convert a model artifact quality application. Where the assessment of the testing of the system stakeholdrs in PT.SP2J. obtained an average satisfaction rate of 90% as for the assessment of availablity system quantitatively compared with Openerp with Openerp 7.0 which only has limited features of 77.7%. Keyword : Enterprise Resoure Planning, Inventory management, Zachman Framwork, UML 2.0 Model Driven Design Openep 7.0. Dalam perencanaan Enterprise Resource planning (ERP), dibutuhkan perencanaan terorganisir, dikarenakan ERP ditunjukan untuk mengintregrasikan seluruh proses yang ada dalam berbagai domain fungsional perusahaan, antar dapartermen, maupun antar lokasi yang berbeda. Penelitian ini bertujuan merancang sebuah desain aplikasi untu k mendapakan blueprint aplaksi pada modul invevtory management (IM) .zachman framework (ZF) merupakan salah satu kerangka kerja yang dapat memetakan artifak arsiktektur informamasi di sebuah organisasi. Dalam menerapnya, ZF mampu mendeskripsikan level prespektif arsitektur IT (planner perspective, owner perspective, Desingner Perspective, Builder Perspective, Implemennter persspective, participant perspective) sesuai abstraksi objek (untuk srandarisasi artifak arsitektur informasi digunakan pendekatan standart pemodelan UML 2.0, (what, How,Where ,Who,When,Why),sehingga mampu meningkatkan deskripsi ZF menjadi standar model Driven Architecture . untuk menguji hasil desain perancangan telah dikembangkan perangkat lunak ERP IM yang menerapkan model Driven Desingn yang mampu mengkonversi artifak model menjadi aplikasi yang berkualitas dimana dari hasil penilaian Stakenholder dari pengujian sistem di PT. SP2J (Sarana Pembangunan Palembang Jaya), didapatkan tingkat kepuasan rata rata 90%. Sedangkan untuk penilaian availdility sistem secara kuantitatif dengan dibandingkan Openerp 7.0 sistem yang dikembangkan jauh lebih komfeleks dengan ketersediaan pitur 88,8% berbanding dengan Opernerp 7.0 yang hanya memiliki keterbatasan fitur 77,7%.

Model of information object for digital library and its verification

An approach for formal verification of UML 2.0 using mapping OWL-DL in UML 2.0 is proposed. As a result, an original approach for mapping OWL-DL to UML 2.0 through description logic has been proposed. The completeness of the mapping of UML-OWL through stereotypes and labeled UML 2.0 values at the level of M0, M1 of the MOF metamodel is provided. A model of the information object (IO) for the semantic electronic library, which is described by using the UML language, is proposed. The proposed IO model was also verified by mapping it into OWL and then validating the constructed ontology by using risoners.

Challenges in Developing Sequence Diagrams (UML)

During the object-oriented software design phase, the designers have to describe the dynamic aspect of the system under development through the most common interaction diagram variant in UML 2.0, i.e. sequence diagrams. Some novice designers, including undergraduate and postgraduate students, suffer from making inappropriate models due to insufficiently detailed guidance required to develop such sequence diagrams. This paper classifies some potential mistakes which are likely performed by such novice designers, and discusses the corresponding corrections. We summarized such mistakes based on our long experiences in teaching software modeling classes as well as software analysis and design classes. There were classified twenty-one potential mistakes with respect to the syntactical and semantical correctness of the developed models. It is concluded that novice designers have to be aware and take into account the identified mistakes in such a way they can produce correct sequence diagrams.

A Method for Modeling and Verifying of UML 2.0 Sequence Diagrams using SPIN

Abstract— This paper proposes a method for modeling and verifying UML 2.0 sequence diagrams using SPIN/PROMELA. The key idea of this method is to generate models that specify behaviors of each object in the given UML 2.0 sequence diagrams. In this paper, I/O automata are used as the models to maintain the interaction among objects. This work also proposes a mechanism to translate these models into PROMELA to use SPIN for checking the correctness of the system. By ensuring software design correctness, several properties can be guaranteed such as safety, stability, and the fact that no vulnerability is left. A support tool for this method is presented and tested with some particular systems to show the accuracy and effectiveness of the proposed method. This approach has promising potential to be applied in practice.Tóm tắt— Bài báo này đề xuất một phương pháp để mô hình hóa và kiểm chứng biểu đồ trình tự UML 2.0 sử dụng SPIN/ PROMELA. Ý tưởng chính của phương pháp là xây dựng các mô hình mô tả hành vi của từng đối tượng trong biểu đồ trình tự UML 2.0. Các mô hình này biểu diễn dưới dạng các ôtômát vào/ra nhằm giữ nguyên tính tương tác giữa các đối tượng. Nghiên cứu đưa ra một kỹ thuật hỗ trợ chuyển đổi các mô hình này thành các đặc tả PROMELA để cung cấp cho bộ công cụ SPIN nhằm kiểm chứng tính đúng đắn của các biểu đồ tuần tự. Bằng cách đảm bảo tính chính xác của thiết kế phần mềm, một số thuộc tính có thể được đảm bảo như an toàn, ổn định và thực tế là không còn lỗ hổng nào. Một công cụ hỗ trợ cho phương pháp đề xuất cũng được cài đặt và thực nghiệm với một số hệ thống điển hình nhằm minh chứng cho tính đúng đắn, hiệu quả và dễ sử dụng. Cách tiếp cận này hứa hẹn sẽ được áp dụng trong thực tế.

RANCANGAN SISTEM PENILAIAN HASIL KINERJA MULTI COMPANY DAN CROSS BUSINESS SECTOR

Each agency has its own characteristics and given authority in managing its finances. Foundation education and welfare PT.PLN (Persero) (YPK-PLN) has 14 affiliated companies. Each affiliate is required to report their financial periodically to YPK-PLN. The diversity of business fields and different locations makes YPK-PLN difficult to obtain financial position data on each affiliate. This financial report becomes one of the YPK-PLN reference to see the state of its subsidiary. The financial statements should be reported quarterly in a year. These financial statements include the balance sheet financial statements, labels and flows. The purpose of this study is to design and build a system that can unify all the financial statements of each affiliate and then calculated the results of its performance. The result of its performance is calculated dimasksud Operating Ratio, Average Collection Period, Return on Equity, Net Profit Margin, Current Ratio and Debt to Equity Ratio. This research was conducted with waterfall methodology to develop the software. To design the system to be built will use UML 2.0. In the development of the software will be used php language with codeigniter framework. The database used is SQL DBMS MariaDB with Apache 2 as its web server. The results also proved that the Performance Results of the affiliate financial ratios have an important role for YPK-PLN in determining whether to invest shares in the company concerned is the right decision.