Siran Lei, Mengqi Cheng and Jianguo Jiang, Department of Mathematics, Liaoning Normal University, Dalian, China
The verification of the correctness of large programs, particularly operating systems is an unmanageable but important endeavor. We are interested in verifying C programs with formal methods, the logic is separation logic, a Hoare-style program logic. In this paper, we present a simple extension of the syntax of separation logic assertion on existing verification system in Coq proof assistant to make assertions more versatile and flexible to describe the state of programs. Moreover, we develop several tactics for proving some related assertions to reduce manual proof as much as possible and improve the efficiency of verification.
Separation Logic, Coq, Interactive Theorem Proving, Program Verification, Automated Reasoning
Howard Dittmer and Xiaoping Jia, School of Computing, College of Computing and Digital Media, DePaul University, Chicago, Illinois, USA
Over time the level of abstraction embodied in programming languages has continued to grow. Yet, most programming languages still require programmers to conform to the language's rigid constructs. These constructs have been implemented in the name of efficiency for the computer. The continual increase in computing power allows us to consider techniques that are no longer limited by this constraint. To this end, we have created CABERNET, a Controlled Nature Language (CNL) approach. CABERNET allows programmers to use a simple outline-based syntax. This allows increased programmer efficiency and syntax flexibility. CNLs have successfully been used for writing requirements documents. We propose taking this approach well beyond this to fully functional programs. Our approach uses heuristics and inference to analyze and determine the programmer's intent. The goal is for programs to be aligned with the way that the humans think rather than the way computers process information.
Controlled Natural Language, Literate Programming, Programming Language, Computer-Aided Software
Mr.Daren Chesworth, Glyndwr University, United Kingdom
The role of maintenance as a ‘non-value’ activity within an organization has evolved over the last half-century. Strategically, it has now become one of the most ‘Smart’ thinking areas of Engineering. This is due to the increased demands by industry to maintain high levels of efficient production whilst providing feedback on equipment performance. The new Industrial Revolution (Industry 4.0) has been driven by technology advances in sensor and wireless data transmission, which has been adopted by those who develop strategies within the organization to provide unprecedented levels of equipment data. Analysed correctly, equipment failures are predicted with greater accuracy which will reduce unplanned machine downtime within a system. This reduction in downtime will increase overall efficiencies which in turn will improve organization profits. This paper builds upon the work of Garg et al (2006) to contemplate whether the more frequently adopted maintenance strategies (often referred as ‘traditional’) remain applicable. This will then develop further to contemplate the use of Industry 4.0 tools and if they inclusion into a Maintenance Management Model and how accessible these new developments are to all industries.
Industry 4.0, IoT, CPS, Big Data, Cloud Computing, Maintenance, Strategy, Industrial Revolution
Sara Beitelspacher, Mohammad Mubashir, Kedir Mamo Besher and Mohammed Zamshed Ali, Erik Jonsson School of Engineering & Computer Science at The University of Texas at Dallas, Tx, USA
While routing through the Internet of Things (IoT) network, conventional healthcare data packets do not get any special priority routing treatment. IoT is facing performance issues in packet data transmission due to network congestion; with the conventional packet routing process, there is no guarantee that the patients’ health data will be properly routed to doctors on time. This leaves the remote medical treatment at risk with possible threat to patients’ lives. In this paper, we studied the current healthcare packet transmission process in IoT and its performance issues in congested IoT networks, then proposed a solution to prioritize healthcare data routing in congested IoT cloud networks. Our proposed system adds a healthcare data identifier in IP packet headers at the sensor level, modifies QoS software at the network router level, and prioritizes healthcare data packet routing based on the healthcare data identifier seen at router QoS. Test data shows promising results that may significantly benefit remote medical diagnostic process by saving time, cost, and more importantly, human lives. The analysis also opens up further avenues for research.
IoT, Priority, Congestion, Interference, Wireless sensor network
Mesmin J. Mbyamm Kiki, ZHANG. Jianbiao, Bonzou Adolphe Kouassi and Sakho Seybou, Beijing University of Technology, 100124 Beijing, China
Smart Cloud Manufacturing System (SCMS) security issues are the bottlenecks that limit the development of smart cloud manufacturing. First of all, based on the security risk matrix of the SCMS architecture, the existing SCMS security system has defects such as centralization, leakage of evidence, and insecurity, credibility of identity authentication, message authentication, and access control. According to the technical characteristics of encryption, development consensus, detrust and anonymity, collective maintenance, immutability, traceability, and programmable smart contracts, it can solve the fascination problem, and proposes a blockchain-based smart cloud manufacturing system security architecture (BCSCMS), and focused on the five aspects of security authentication based on blockchain-based identity authentication, message authentication, access control, evidence protection, and security auditing and early warning. Finally, from information confidentiality, complete annotation, and follow-up tide The four dimensions of sexuality and anonymity demonstrate the security of the framework.
Security Implementation, Blockchain, BCMS Security Architecture.
Ugochukwu O. Matthew2, Jazuli S. Kazaure1, Ibrahim M. Hassan2, Ubochi Chibueze Nwamouh3, 1Department of Electrical & Electronics, Hussaini Adamu Federal Polytechnic, P.M.B 5004, Kazaure, Jigawa State, Nigeria, 2Department of Computer Science, Hussaini Adamu Federal Polytechnic, P.M.B 5004, Kazaure, Jigawa State, Nigeria and 3Department of Computer Engineering, Michael Okpala University Agriculture, Umudike, Abia State , Nigeria
Enterprise Data Warehousing is a top level Strategic Business and Information Technology (IT) investment in any organization that is technologically, profit driven and customer oriented. Data Warehouses can be developed in two alternative ways through constructing Data Marts and the Enterprise-Wide Data Warehouse strategies, and each has advantages and disadvantages. To create a Data Warehouse, Data must be extracted from multiple heterogeneous source systems, Transformed, Cleaned and Loaded to an Appropriate Data Store. Depending on the business requirements, either relational or multidimensional database technology can be used for the data stores. To provide a multidimensional view of the data using a relational database, a star schema data model architecture is used for the data federation implementation. Online analytical processing (OLAP) can be performed on both kinds of Repository technology. The Metadata and Data attributes about the data in the Data Warehouse Repository is important for IT and end users specifications. Some reasonable number of database access tools and applications can be used in conjunction with Data Warehouse; which may include Structured Query Language (SQL) queries, Management Reporting Systems, Enterprise Query environments, Decision Support System/Executive Information System, Enterprise Intelligence Portals, Data Mining, and Customer Relationship Management for effective and optimizable Information Retrieval, Indexing and Enterprise Business Decision. The central aim of this paper is to develop an Enterprise Data warehouse to speed up Research, as well as connect Medical Researchers from around the world through the existence of the Medical Data Warehouses and Data Marts as Medical Solutions and Clinical information will be archived for daily use up to the next generation . This will enable focus to be narrowed as manpower multiplies in finding answers to certain medical mysteries. Standard operational Procedures will be improved as people will be allowed to access the web portals for the past Medical and clinical solution to all research articles wherever it existed.
Data Mining, Data Warehouse, Cloud Computing, Internet of Things (IOTs) & ICT
Donatien Niyonzima and Kriti Bhuju, Institute of Communication Studies, Communication University of China, Beijing, China
By using Big Data, Advanced Analytics and Artificial Intelligence, Chinese Media and communication companies have taken advantage of the potential of these technologies to improve their capability to know how to communicate to the world and optimize strategically their message and policy contents. AI offers huge promise for media companies – yet success to date has been reserved for the pioneering few. Hence, this study has tried to find out status of AI use in Chinese media and explore new media roles made possible by its use. Some of the most important tasks AI has helped in the journalistic works are object extraction and automated tagging, automated fact checking, content moderation, speech-to-text (mostly English for now) and ad targeting among others. The media in China has been using AI for all these works and are far ahead of media around the world in terms of AI adoption in media.
Artificial Intelligence, Media, Global Communication, Content Optimization, Automation
Samar Mouti and Samer Rihawi, Department of Information Technology, Khawarizmi College, Abu Dhabi, UAE
This paper describes the UAE Sign Language (USL) System in a real domain for deaf-mute people. USL system is useful for the interaction of the deaf with the community. The USL system is an expert system translates speech into UAE Sign Language. This system is composed of speech recognizer, natural language translator, and video generator. Speech recognizer for decoding the spoken utterance into a written text. A natural language translator for converting a written text into a sequence of videos of the UAE sign language using video generator.
Speech Recognition, UAE Sign Language, Python, Expert System, Natural Language Processing
Raja Muhammad Suleman and Yannis Korkontzelos, Department of Computer Science, Edge Hill University,Ormskirk, Lancashire L39 4QP, United Kingdom
Natural Language Processing (NLP) is a sub-field of Artificial Intelligence that is used for analysing and representing human language automatically. NLP has been employed in many applications, such as information retrieval, information processing, automated answer grading etc. Several approaches have been developed for understanding the meaning of text, commonly known as semantic analysis. Latent Semantic Analysis (LSA) is a widely used corpus-based approach that evaluates similarity of text on the basis of semantic relations among words. LSA has been used successfully in different language systems for calculating the semantic similarity of texts. However, LSA ignores the structural composition of sentences and therefore this technique suffers from the syntactic blindness problem. LSA fails to distinguish between sentences that contain semantically similar words but have completely opposite meaning. LSA is also blind to the syntactic structure of a sentence and therefore cannot differentiate between sentences and lists of keywords. In such a situation, the comparison between a sentence and a list of keywords without any syntactic structure gets a high similarity score. In this research we propose an extension of Latent Semantic Analysis (xLSA) which focuses on syntactic composition of a sentence to overcome LSA’s syntactic blindness problems. xLSA was tested on sentence pairs containing similar words but having different meaning. Our results showed that our extension allows LSA to manage the syntactic blindness problem to provide more realistic semantic similarity scores.
Natural Language Processing, Natural Language Understanding, Latent Semantic Analysis, Semantic Similarity.
Manaswini R., Saikrishna B., Nishu Gupta, Electronics and Communication Engineering Department, Vaagdevi College of Engineering, Warangal, India
Internet of things (IoT) enables exchanging of various entities like smart health, smart industry and smart home development. These systems have already gained popularity and is still increasing day by day. Moving ahead, we need to develop a transport system all over the world with the help of IoT sensors technology. A new diversity leads to the introduction of Internet of Vehicles (IoV). IoV facilitates communication between Vehicle to Vehicle, Vehicle to Sensors and Vehicle to Roadside unit (RSU) with the help of artificial intelligence. It forms a solid backbone for Intelligent transportation systems (ITS) which gives further insight to the technologies that better explain about traffic efficiency and their management applications. In this article, a novel approach towards architecture model, frameworl, cross-level interaction, applications and challenges of IoV are discussed in the context of ITS and future vehicular scenario.
Artificial Intelligence, Cloud Computing, Internet of Vehicles, Internet of Things, Intelligent Transportation System, VANET
Shirokanev Alexander1,2, Kibitkina Alena2, Ilyasova Nataly1,2 and Zamyckij Evgeny3, 1IPSI RAS - branch of the FSRC «Crystallography and Photonics» RAS, Molodogvardejskaya street 151, Samara, Russia, 443001, 2Samara National Research University, Moskovskoe Shosse 34A, Samara, Russia, 443086 and 3Samara State Medical University, Chapayevskaya street 89, Samara, Russia, 443099
Diabetic retinopathy is frequent, the most dangerous fundus disease. Diabetic retinopathy can result in many serious diseases. For various reasons, patients lose vision in untimely or incorrect treatment of diabetic retinopathy. The current method of treating diabetic retinopathy is laser coagulation. The ophthalmologist decides which zones need to be shelled to reduce edema based on his experience. Laser radiation parameters and distance between laser shots are also selected based on the experience of previous operations. However, the accuracy of the selection of these parameters can affect the result of treatment. Achieving high accuracy is empirical difficult. The present paper proposes a technology for selecting an effective laser coagulation strategy consisting in application of a genetic efficiency optimization algorithm based on solving of the problems of mathematical simulation of laser burns. Technology solves the problem of choosing accurate laser coagulation parameters.
Diabetic retinopathy, laser coagulation, ocular fundus, information technology, mathematical modeling, thermal conductivity equation
Ahed Abugabah, Nishara Nizamuddin, Alaa Abugabah, College of Technological Innovation, Zayed University, Abu Dhabi, United Arab Emirates
The healthcare industry is progressively involved in adopting new technologies to provide improved quality of care given to patients. The implementation of RFID technology has globally impacted several industries and this revolution has improved the aspects of service delivery in the healthcare industry as well. The RFID technology has the potential to track medical assets and interact with almost any of the medical devices, pharmaceutical materials, IT equipment, or individual patients, deployed in hospitals all over the world. The motivation behind this paper is to investigate the advantages and obstacles to implement RFID technology in the healthcare sector highlighted in the literature. Further, we highlight the most possible methods or technologies to be adapted to overcome the limitations of implementation.
Jihane LARIOUI1 and Abdeltif EL BYED2, 1Laboratory LIMSAD, Hassan 2University, Faculty Of Science Ain Chock Casablanca, Morocco
Over time, intelligent transport systems (ITS) have shown their relevance and have become essential for good urban mobility management within smart cities. They facilitate traffic management and make flow more fluid and autonomous. Indeed, the data manipulated in the ITS is large and diver-sified which makes the information less exploitable and leads us to a consid-erable loss of time before obtaining the desired information .In the literature, no formal semantics describing all aspects relating to intelligent road transport systems have been proposed. Thus, the objective of this semantic approach is to localize the different resources of the WEB, to standardize the description models so that they are understandable and usable by the differ-ent agents of the system. In this article, we have proposed a new approach for the development of an architecture based on Multi- Agent systems (SMA) coupled with semantic Web services (SWS) and this in order to help decision- making in the context of urban mobility. Thus, We are implementing an ontology for the multi-modal transport system aimed at improving the management of urban mo-bility, covering all modes of transport and capable of managing planned trips as well as answering questions related to safety during travel.
Multi-agent System (SMA), Intelligent transport systems (ITS), Ontology, Semantic Web, Multi-modal Transportation
Henry Collier1 and Alexandra Collier2, 1College of Graduate and Continuing Studies, Norwich University, Northfield, Vermont, USA and 2Southern New Hampshire University, Manchester, New Hampshire, USA
Current practices to defend networks against threats involves hardening systems by limiting points of ingress into the system. The most common method of limiting ingress into a system is by limiting which ports are allowed through the firewall. Port limitation as a method of defense is normally effective. Ports in a firewall range from 0 through 65,535 and covers the technical aspects of information security. One method of ingress not covered by technical ports is the human port, coined “port Z3r0” for this paper. To better defend against port Z3r0, we must understand the human better and why they are susceptible. This paper explores the basic human behaviors related to susceptibility and identifies classifications of traits that increase a person’s susceptibility level. Additionally, this paper will address the issue of how the current model of teaching end users to defend themselves is lacking and needs to be improved.
Information Security, Non-Malicious Insider Threat, Susceptibility,Human Behaviors, Cognition